1  /-
  2  Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Robert Y. Lewis
  5  
  6  -/
  7  
  8  import data.real.cau_seq_completion
src         └──────────────────────────┘
  9  import data.padics.padic_norm algebra.archimedean analysis.normed_space.basic
src         └────────────────────┘ └─────────────────┘ └─────────────────────────┘
 10  import tactic.norm_cast
src         └──────────────┘
 11  
 12  /-!
 13  # p-adic numbers
 14  
 15  This file defines the p-adic numbers (rationals) ℚ_p as the completion of ℚ with respect to the
 16  p-adic norm. We show that the p-adic norm on ℚ extends to ℚ_p, that ℚ is embedded in ℚ_p, and that
 17  ℚ_p is Cauchy complete.
 18  
 19  ## Important definitions
 20  
 21  * `padic` : the type of p-adic numbers
 22  * `padic_norm_e` : the rational valued p-adic norm on ℚ_p
 23  
 24  ## Notation
 25  
 26  We introduce the notation ℚ_[p] for the p-adic numbers.
 27  
 28  ## Implementation notes
 29  
 30  Much, but not all, of this file assumes that `p` is prime. This assumption is inferred automatically
 31  by taking (prime p) as a type class argument.
 32  
 33  We use the same concrete Cauchy sequence construction that is used to construct ℝ. ℚ_p inherits a
 34  field structure from this construction. The extension of the norm on ℚ to ℚ_p is *not* analogous to
 35  extending the absolute value to ℝ, and hence the proof that ℚ_p is complete is different from the
 36  proof that ℝ is complete.
 37  
 38  A small special-purpose simplification tactic, `padic_index_simp`, is used to manipulate sequence
 39  indices in the proof that the norm extends.
 40  
 41  `padic_norm_e` is the rational-valued p-adic norm on ℚ_p. To instantiate ℚ_p as a normed field, we
 42  must cast this into a ℝ-valued norm. The ℝ-valued norm, using notation ∥ ∥ from normed spaces, is
 43  the canonical representation of this norm.
 44  
 45  Coercions from ℚ to ℚ_p are set up to work with the `norm_cast` tactic.
 46  
 47  ## References
 48  
 49  * [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
 50  * [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
 51  * <https://en.wikipedia.org/wiki/P-adic_number>
 52  
 53  ## Tags
 54  
 55  p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion
 56  -/
 57  
 58  noncomputable theory
 59  open_locale classical
 60  
 61  open nat multiplicity padic_norm cau_seq cau_seq.completion metric
 62  
 63  /-- The type of Cauchy sequences of rationals with respect to the p-adic norm. -/
 64  @[reducible] def padic_seq (p : ℕ) [p.prime] := cau_seq _ (padic_norm p)
id                                      └────┘     └─────┘    └────────┘ 
src                                      └────┘     └─────┘    └────────┘
typ                                     └────┘     └─────┘    └────────┘ 
doc    └───────┘                          └────┘                └────────┘
 65  
 66  namespace padic_seq
 67  
 68  section
 69  variables {p : ℕ} [nat.prime p]
id                     └───────┘
src                    └───────┘
typ                    └───────┘
doc                     └───────┘
 70  
 71  /-- The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually
 72  constant. -/
 73  lemma stationary {f : cau_seq ℚ (padic_norm p)} (hf : ¬ f ≈ 0) :
id                         └─────┘   └────────┘            
src                        └─────┘   └────────┘              
typ                        └─────┘   └────────┘            
doc                                  └────────┘
 74    ∃ N, ∀ m n, N ≤ m → N ≤ n → padic_norm p (f n) = padic_norm p (f m) :=
id                      └────────┘       └────────┘    
src                            └────────┘          └────────┘
typ                     └────────┘       └────────┘    
doc                                └────────┘           └────────┘
 75  have ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padic_norm p (f j),
id               └┘      └┘    └────────┘    
src                              └────────┘
typ              └┘      └┘    └────────┘    
doc                                    └────────┘
 76    from cau_seq.abv_pos_of_not_lim_zero $ not_lim_zero_of_not_congr_zero hf,
id          └─────────────────────────────┘   └────────────────────────────┘ └┘
src         └─────────────────────────────┘   └────────────────────────────┘
typ         └─────────────────────────────┘   └────────────────────────────┘ └┘
 77  let ⟨ε, hε, N1, hN1⟩ := this,
id   └─┘    └┘  └┘  └─┘     └──┘
typ  └─┘    └┘  └┘  └─┘     └──┘
 78      ⟨N2, hN2⟩ := cau_seq.cauchy₂ f hε in
id        └┘  └─┘     └─────────────┘ 
src                   └─────────────┘
typ       └┘  └─┘     └─────────────┘ 
 79  ⟨ max N1 N2,
id     └─┘
src    └─┘
typ    └─┘
 80    λ n m hn hm,
id         └┘ └┘
typ        └┘ └┘
 81    have padic_norm p (f n - f m) < ε, from hN2 _ _ (max_le_iff.1 hn).2 (max_le_iff.1 hm).2,
id          └────────┘                           └────────┘  └┘    └────────┘  └┘ 
src         └────────┘                                └────────┘        └────────┘     
typ         └────────┘                           └────────┘  └┘    └────────┘  └┘ 
doc         └────────┘
 82    have padic_norm p (f n - f m) < padic_norm p (f n),
id          └────────┘          └────────┘    
src         └────────┘               └────────┘
typ         └────────┘          └────────┘    
doc         └────────┘                 └────────┘
 83      from lt_of_lt_of_le this $ hN1 _ (max_le_iff.1 hn).1,
id            └────────────┘ └──┘          └────────┘  └┘ 
src           └────────────┘               └────────┘     
typ           └────────────┘ └──┘          └────────┘  └┘ 
 84    have  padic_norm p (f n - f m) < max (padic_norm p (f n)) (padic_norm p (f m)),
id           └────────┘          └─┘  └────────┘        └────────┘    
src          └────────┘               └─┘  └────────┘           └────────┘
typ          └────────┘          └─┘  └────────┘        └────────┘    
doc          └────────┘                      └────────┘           └────────┘
 85      from lt_max_iff.2 (or.inl this),
id            └────────┘   └────┘ └──┘
src           └────────┘   └────┘
typ           └────────┘   └────┘ └──┘
 86    begin
st     └─────
 87      by_contradiction hne,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid                      └──┘
st   ───────────────────────┘└─
 88      rw ←padic_norm.neg p (f m) at hne,
id           └────────────┘    
src      └──┘└────────────┘    └──────┘
typ      └──┘└────────────┘ └──────┘
doc      └──┘└────────────┘    └──────┘
txt      └──┘                  └──────┘
par      └──┘                  └──────┘
pid        └┘                  └─────┘
st   ────────────────────────────────────┘└─
 89      have hnam := add_eq_max_of_ne p hne,
id                    └──────────────┘  └─┘
src      └───────────┘└──────────────┘ 
typ      └───────────┘└──────────────┘└─┘
doc      └───────────┘└──────────────┘ 
txt      └───────────┘                 
par      └───────────┘                 
pid      └───────┘└─┘                 
st   ──────────────────────────────────────┘└─
 90      rw [padic_norm.neg, max_comm] at hnam,
id           └────────────┘  └──────┘
src      └──┘└────────────┘└┘└──────┘└───────┘
typ      └──┘└────────────┘└┘└──────┘└───────┘
doc      └──┘└────────────┘└┘        └───────┘
txt      └──┘              └┘        └───────┘
par      └──┘              └┘        └───────┘
pid        └┘              └┘        └──────┘
st   ─────────────────────┘└────────┘└──────┘└─
 91      rw ←hnam at this,
id           └──┘
src      └──┘    └──────┘
typ      └──┘└──┘└──────┘
doc      └──┘    └──────┘
txt      └──┘    └──────┘
par      └──┘    └──────┘
pid        └┘    └──────┘
st   ───────────────────┘└─
 92      apply _root_.lt_irrefl _ (by simp at this; exact this)
id             └──────────────┘                           └──┘
src      └────┘└──────────────┘└─┘   └──────────┘└┘└────┘    └─
typ      └────┘└──────────────┘└─┘   └──────────┘└──────┘└──┘└─
doc      └────┘                └─┘   └──────────┘└┘└────┘    └─
txt      └────┘                └─┘   └──────────┘└┘└────┘    └─
par      └────┘                └─┘   └──────────┘└──────┘    └─
pid                           └─┘   └───────────────────┘    
st   ───────────────────────────────┘└───────────────────────┘└─
 93    end ⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 94  
 95  /-- For all n ≥ stationary_point f hf, the p-adic norm of f n is the same. -/
 96  def stationary_point {f : padic_seq p} (hf : ¬ f ≈ 0) : ℕ :=
id                             └───────┘                 
src                            └───────┘                   
typ                            └───────┘                 
doc                            └───────┘
 97  classical.some $ stationary hf
id   └────────────┘   └────────┘ └┘
src  └────────────┘   └────────┘
typ  └────────────┘   └────────┘ └┘
doc                   └────────┘
 98  
 99  lemma stationary_point_spec {f : padic_seq p} (hf : ¬ f ≈ 0) :
id                                    └───────┘           
src                                   └───────┘             
typ                                   └───────┘           
doc                                   └───────┘
100    ∀ {m n}, m ≥ stationary_point hf → n ≥ stationary_point hf →
id              └──────────────┘ └┘     └──────────────┘ └┘
src                └──────────────┘         └──────────────┘
typ             └──────────────┘ └┘     └──────────────┘ └┘
doc                 └──────────────┘          └──────────────┘
101      padic_norm p (f n) = padic_norm p (f m) :=
id       └────────┘       └────────┘    
src      └────────┘          └────────┘
typ      └────────┘       └────────┘    
doc      └────────┘           └────────┘
102  classical.some_spec $ stationary hf
id   └─────────────────┘   └────────┘ └┘
src  └─────────────────┘   └────────┘
typ  └─────────────────┘   └────────┘ └┘
doc                        └────────┘
103  
104  /-- Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm
105  to sequences. -/
106  def norm (f : padic_seq p) : ℚ :=
id                 └───────┘     
src                └───────┘      
typ                └───────┘     
doc                └───────┘      
107  if hf : f ≈ 0 then 0 else padic_norm p (f (stationary_point hf))
id   └┘                      └────────┘     └──────────────┘ └┘
src  └┘                       └────────┘       └──────────────┘
typ  └┘                      └────────┘     └──────────────┘ └┘
doc                            └────────┘       └──────────────┘
108  
109  lemma norm_zero_iff (f : padic_seq p) : f.norm = 0 ↔ f ≈ 0 :=
id                            └───────┘     └───┘      
src                           └───────┘       └───┘       
typ                           └───────┘     └───┘      
doc                           └───────┘       └───┘
110  begin
st   └─────
111    constructor,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
st   ────────────┘└─
112    { intro h,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
113      by_contradiction hf,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid                      └─┘
st   ──────────────────────┘└─
114      unfold norm at h, split_ifs at h,
src      └──────────────┘  └────────────┘
typ      └──────────────┘  └────────────┘
doc      └──────────────┘  └────────────┘
txt      └──────────────┘  └────────────┘
par      └──────────────┘  └────────────┘
pid            └───┘└───┘           └───┘
st   ───────────────────┘└──────────────┘└─
115      apply hf,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
116      intros ε hε,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
117      existsi stationary_point hf,
id               └──────────────┘ └┘
src      └──────┘└──────────────┘
typ      └──────┘└──────────────┘└┘
doc      └──────┘└──────────────┘
txt      └──────┘                
par      └──────┘                
pid                             
st   ──────────────────────────────┘└─
118      intros j hj,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
119      have heq := stationary_point_spec hf (le_refl _) hj,
id                   └───────────────────┘ └┘  └─────┘    └┘
src      └──────────┘└───────────────────┘   └─────┘└──┘
typ      └──────────┘└───────────────────┘└┘ └─────┘└──┘└┘
doc      └──────────┘                               └──┘
txt      └──────────┘                               └──┘
par      └──────────┘                               └──┘
pid      └──────┘└─┘                               └──┘
st   ──────────────────────────────────────────────────────┘└─
120      simpa [h, heq] },
id                └─┘
src      └─────┘ └┘└─┘└┘
typ      └─────┘└┘└─┘└┘
doc      └─────┘ └┘   └┘
txt      └─────┘ └┘   └┘
par      └─────┘ └┘   └┘
pid            └┘   
st   ──────────────────┘└┘
121    { intro h,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
122      simp [norm, h] }
id             └──┘  
src      └────┘└──┘└┘ └┘
typ      └────┘└──┘└┘└┘
doc      └────┘└──┘└┘ └┘
txt      └────┘    └┘ └┘
par      └────┘    └┘ └┘
pid              └┘ 
st   ──────────────────┘└─
123  end
st   ──┘
124  
125  end
126  
127  section embedding
128  open cau_seq
129  variables {p : ℕ} [nat.prime p]
id                     └───────┘
src                    └───────┘
typ                    └───────┘
doc                     └───────┘
130  
131  lemma equiv_zero_of_val_eq_of_equiv_zero {f g : padic_seq p}
id                                                   └───────┘ 
src                                                  └───────┘
typ                                                  └───────┘ 
doc                                                  └───────┘
132    (h : ∀ k, padic_norm p (f k) = padic_norm p (g k)) (hf : f ≈ 0) : g ≈ 0 :=
id              └────────┘       └────────┘                     
src              └────────┘          └────────┘                          
typ             └────────┘       └────────┘                     
doc              └────────┘           └────────┘
133  λ ε hε, let ⟨i, hi⟩ := hf _ hε in
id      └┘  └─┘           └┘   └┘
typ     └┘  └─┘           └┘   └┘
134  ⟨i, λ j hj, by simpa [h] using hi _ hj⟩
id          └┘                    └┘   └┘
src                 └─────┘ └──────┘  └─┘
typ         └┘     └─────┘└──────┘└┘└─┘└┘
doc                 └─────┘ └──────┘  └─┘
txt                 └─────┘ └──────┘  └─┘
par                 └─────┘ └──────┘  └─┘
pid                       └────┘  └─┘
st                 └──────────────────────┘
135  
136  lemma norm_nonzero_of_not_equiv_zero {f : padic_seq p} (hf : ¬ f ≈ 0) :
id                                             └───────┘           
src                                            └───────┘             
typ                                            └───────┘           
doc                                            └───────┘
137    f.norm ≠ 0 :=
id     └───┘ 
src     └───┘ 
typ    └───┘ 
doc     └───┘
138  hf ∘ f.norm_zero_iff.1
id   └┘  └────────────┘
src       └────────────┘
typ  └┘  └────────────┘
139  
140  lemma norm_eq_norm_app_of_nonzero {f : padic_seq p} (hf : ¬ f ≈ 0) :
id                                          └───────┘           
src                                         └───────┘             
typ                                         └───────┘           
doc                                         └───────┘
141    ∃ k, f.norm = padic_norm p k ∧ k ≠ 0 :=
id       └───┘  └────────┘     
src        └───┘  └────────┘        
typ      └───┘  └────────┘     
doc          └───┘   └────────┘
142  have heq : f.norm = padic_norm p (f $ stationary_point hf), by simp [norm, hf],
id              └───┘  └────────┘      └──────────────┘ └┘            └──┘  └┘
src              └───┘  └────────┘        └──────────────┘         └────┘└──┘└┘  
typ             └───┘  └────────┘      └──────────────┘ └┘      └────┘└──┘└┘└┘
doc              └───┘   └────────┘        └──────────────┘         └────┘└──┘└┘  
txt                                                                 └────┘    └┘  
par                                                                 └────┘    └┘  
pid                                                                         └┘  
st                                                                 └──────────────┘
143  ⟨f $ stationary_point hf, heq,
id       └──────────────┘ └┘  └─┘
src       └──────────────┘     └─┘
typ      └──────────────┘ └┘  └─┘
doc       └──────────────┘
144    λ h, norm_nonzero_of_not_equiv_zero hf (by simpa [h] using heq)⟩
id         └────────────────────────────┘ └┘                    └─┘
src         └────────────────────────────┘        └─────┘ └──────┘└─┘
typ        └────────────────────────────┘ └┘     └─────┘└──────┘└─┘
doc                                               └─────┘ └──────┘
txt                                               └─────┘ └──────┘
par                                               └─────┘ └──────┘
pid                                                     └────┘
st                                               └──────────────────┘
145  
146  lemma not_lim_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬ lim_zero (const (padic_norm p) q) :=
id                                                            └──────┘  └───┘  └────────┘   
src                                                            └──────┘  └───┘  └────────┘
typ                                                           └──────┘  └───┘  └────────┘   
doc                                                              └──────┘  └───┘  └────────┘
147  λ h', hq $ const_lim_zero.1 h'
id     └┘  └┘   └────────────┘  └┘
src             └────────────┘
typ    └┘  └┘   └────────────┘  └┘
148  
149  lemma not_equiv_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬ (const (padic_norm p) q) ≈ 0 :=
id                                                               └───┘  └────────┘     
src                                                               └───┘  └────────┘       
typ                                                              └───┘  └────────┘     
doc                                                                 └───┘  └────────┘
150  λ h : lim_zero (const (padic_norm p) q - 0), not_lim_zero_const_of_nonzero hq $ by simpa using h
id         └──────┘  └───┘  └────────┘         └───────────────────────────┘ └┘                  
src        └──────┘  └───┘  └────────┘           └───────────────────────────┘         └──────────┘ 
typ        └──────┘  └───┘  └────────┘         └───────────────────────────┘ └┘      └──────────┘
doc        └──────┘  └───┘  └────────┘                                                  └──────────┘ 
txt                                                                                     └──────────┘ 
par                                                                                     └──────────┘ 
pid                                                                                          └────┘ 
st                                                                                     └──────────────
151  
src  
typ  
doc  
txt  
par  
pid  
st   
152  lemma norm_nonneg (f : padic_seq p) : f.norm ≥ 0 :=
id                          └───────┘     └───┘ 
src                         └───────┘       └───┘ 
typ                         └───────┘     └───┘ 
doc                         └───────┘       └───┘
153  if hf : f ≈ 0 then by simp [hf, norm]
id   └┘                        └┘  └──┘
src  └┘                   └────┘  └┘└──┘└┘
typ  └┘                  └────┘└┘└┘└──┘└┘
doc                        └────┘  └┘└──┘└┘
txt                        └────┘  └┘    └┘
par                        └────┘  └┘    └┘
pid                              └┘    
st                        └───────────────┘
154  else by simp [norm, hf, padic_norm.nonneg]
id                 └──┘  └┘  └───────────────┘
src          └────┘└──┘└┘  └┘└───────────────┘└─
typ          └────┘└──┘└┘└┘└┘└───────────────┘└─
doc          └────┘└──┘└┘  └┘└───────────────┘└─
txt          └────┘    └┘  └┘                 └─
par          └────┘    └┘  └┘                 └─
pid                  └┘  └┘                 
st          └───────────────────────────────────
155  
src  
typ  
doc  
txt  
par  
pid  
st   
156  /-- An auxiliary lemma for manipulating sequence indices. -/
157  lemma lift_index_left_left {f : padic_seq p} (hf : ¬ f ≈ 0) (v2 v3 : ℕ) :
id                                   └───────┘                        
src                                  └───────┘                          
typ                                  └───────┘                        
doc                                  └───────┘
158    padic_norm p (f (stationary_point hf)) =
id     └────────┘     └──────────────┘ └┘   
src    └────────┘       └──────────────┘      
typ    └────────┘     └──────────────┘ └┘   
doc    └────────┘       └──────────────┘
159      padic_norm p (f (max (stationary_point hf) (max v2 v3))) :=
id       └────────┘     └─┘  └──────────────┘ └┘   └─┘ └┘ └┘
src      └────────┘       └─┘  └──────────────┘      └─┘
typ      └────────┘     └─┘  └──────────────┘ └┘   └─┘ └┘ └┘
doc      └────────┘            └──────────────┘
160  let i := max (stationary_point hf) (max v2 v3) in
id           └─┘  └──────────────┘ └┘   └─┘ └┘ └┘
src           └─┘  └──────────────┘      └─┘
typ          └─┘  └──────────────┘ └┘   └─┘ └┘ └┘
doc                └──────────────┘
161  begin
st   └─────
162    apply stationary_point_spec hf,
id           └───────────────────┘ └┘
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘└┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ───────────────────────────────┘└─
163    { apply le_max_left },
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘           
txt      └────┘           
par      └────┘           
pid                      
st   ───┘└────────────────┘└┘
164    { apply le_refl }
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ─────────────────┘└─
165  end
st   ──┘
166  
167  /-- An auxiliary lemma for manipulating sequence indices. -/
168  lemma lift_index_left {f : padic_seq p} (hf : ¬ f ≈ 0) (v1 v3 : ℕ) :
id                              └───────┘                        
src                             └───────┘                          
typ                             └───────┘                        
doc                             └───────┘
169    padic_norm p (f (stationary_point hf)) =
id     └────────┘     └──────────────┘ └┘   
src    └────────┘       └──────────────┘      
typ    └────────┘     └──────────────┘ └┘   
doc    └────────┘       └──────────────┘
170      padic_norm p (f (max v1 (max (stationary_point hf) v3))) :=
id       └────────┘     └─┘ └┘  └─┘  └──────────────┘ └┘  └┘
src      └────────┘       └─┘     └─┘  └──────────────┘
typ      └────────┘     └─┘ └┘  └─┘  └──────────────┘ └┘  └┘
doc      └────────┘                    └──────────────┘
171  let i := max v1 (max (stationary_point hf) v3) in
id           └─┘ └┘  └─┘  └──────────────┘ └┘  └┘
src           └─┘     └─┘  └──────────────┘
typ          └─┘ └┘  └─┘  └──────────────┘ └┘  └┘
doc                        └──────────────┘
172  begin
st   └─────
173    apply stationary_point_spec hf,
id           └───────────────────┘ └┘
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘└┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ───────────────────────────────┘└─
174    { apply le_trans,
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└────────────┘└─
175      { apply le_max_left _ v3 },
id               └─────────┘   └┘
src        └────┘└─────────┘└─┘  
typ        └────┘└─────────┘└─┘└┘
doc        └────┘           └─┘  
txt        └────┘           └─┘  
par        └────┘           └─┘  
pid                        └─┘  
st   ─────┘└─────────────────────┘└┘
176      { apply le_max_right } },
id               └──────────┘
src        └────┘└──────────┘
typ        └────┘└──────────┘
doc        └────┘            
txt        └────┘            
par        └────┘            
pid                         
st   ────────────────────────┘└──┘
177    { apply le_refl }
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ─────────────────┘└─
178  end
st   ──┘
179  
180  /-- An auxiliary lemma for manipulating sequence indices. -/
181  lemma lift_index_right {f : padic_seq p} (hf : ¬ f ≈ 0) (v1 v2 : ℕ) :
id                               └───────┘                        
src                              └───────┘                          
typ                              └───────┘                        
doc                              └───────┘
182    padic_norm p (f (stationary_point hf)) =
id     └────────┘     └──────────────┘ └┘   
src    └────────┘       └──────────────┘      
typ    └────────┘     └──────────────┘ └┘   
doc    └────────┘       └──────────────┘
183      padic_norm p (f (max v1 (max v2 (stationary_point hf)))) :=
id       └────────┘     └─┘ └┘  └─┘ └┘  └──────────────┘ └┘
src      └────────┘       └─┘     └─┘     └──────────────┘
typ      └────────┘     └─┘ └┘  └─┘ └┘  └──────────────┘ └┘
doc      └────────┘                       └──────────────┘
184  let i := max v1 (max v2 (stationary_point hf)) in
id           └─┘ └┘  └─┘ └┘  └──────────────┘ └┘
src           └─┘     └─┘     └──────────────┘
typ          └─┘ └┘  └─┘ └┘  └──────────────┘ └┘
doc                           └──────────────┘
185  begin
st   └─────
186    apply stationary_point_spec hf,
id           └───────────────────┘ └┘
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘└┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ───────────────────────────────┘└─
187    { apply le_trans,
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└────────────┘└─
188      { apply le_max_right v2 },
id               └──────────┘ └┘
src        └────┘└──────────┘  
typ        └────┘└──────────┘└┘
doc        └────┘              
txt        └────┘              
par        └────┘              
pid                           
st   ─────┘└────────────────────┘└┘
189      { apply le_max_right } },
id               └──────────┘
src        └────┘└──────────┘
typ        └────┘└──────────┘
doc        └────┘            
txt        └────┘            
par        └────┘            
pid                         
st   ────────────────────────┘└──┘
190    { apply le_refl }
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ─────────────────┘└─
191  end
st   ──┘
192  
193  end embedding
194  
195  end padic_seq
196  
197  section
198  open padic_seq
199  
200  private meta def index_simp_core (hh hf hg : expr)
id                                                └──┘
src                                               └──┘
typ                                               └──┘
doc                                               └──┘
201    (at_ : interactive.loc := interactive.loc.ns [none]) : tactic unit :=
id            └─────────────┘    └────────────────┘ └──┘    └────┘ └──┘
src           └─────────────┘    └────────────────┘ └──┘    └────┘ └──┘
typ           └─────────────┘    └────────────────┘ └──┘    └────┘ └──┘
doc                              └────────────────┘                  └──┘
202  do [v1, v2, v3] ← [hh, hf, hg].mmap
id      └┘ └┘ └┘   └┘ └┘ └┘└──┘
src                        └──┘
typ     └┘ └┘ └┘   └┘ └┘ └┘└──┘
203       (λ n, tactic.mk_app ``stationary_point [n] <|> return n),
id             └───────────┘                    └─┘ └────┘ 
src             └───────────┘                     └─┘ └────┘
typ            └───────────┘                    └─┘ └────┘ 
doc             └───────────┘
204     e1 ← tactic.mk_app ``lift_index_left_left [hh, v2, v3] <|> return `(true),
id      └┘   └───────────┘                       └┘       └─┘ └────┘   └──┘
src          └───────────┘                                └─┘ └────┘   └──┘
typ     └┘   └───────────┘                       └┘       └─┘ └────┘   └──┘
doc          └───────────┘
205     e2 ← tactic.mk_app ``lift_index_left [hf, v1, v3] <|> return `(true),
id      └┘   └───────────┘                  └┘       └─┘ └────┘   └──┘
src          └───────────┘                           └─┘ └────┘   └──┘
typ     └┘   └───────────┘                  └┘       └─┘ └────┘   └──┘
doc          └───────────┘
206     e3 ← tactic.mk_app ``lift_index_right [hg, v1, v2] <|> return `(true),
id      └┘   └───────────┘                   └┘       └─┘ └────┘   └──┘
src          └───────────┘                            └─┘ └────┘   └──┘
typ     └┘   └───────────┘                   └┘       └─┘ └────┘   └──┘
doc          └───────────┘
207     sl ← [e1, e2, e3].mfoldl (λ s e, simp_lemmas.add s e) simp_lemmas.mk,
id      └┘   └┘ └┘ └┘└────┘        └─────────────┘    └────────────┘
src                  └────┘          └─────────────┘      └────────────┘
typ     └┘   └┘ └┘ └┘└────┘        └─────────────┘    └────────────┘
208     when at_.include_goal (tactic.simp_target sl),
id      └──┘ └─┘└───────────┘  └────────────────┘ └┘
src     └──┘    └───────────┘  └────────────────┘
typ     └──┘ └─┘└───────────┘  └────────────────┘ └┘
209     hs ← at_.get_locals, hs.mmap' (tactic.simp_hyp sl [])
id      └┘   └─┘└─────────┘  └┘└────┘  └─────────────┘ └┘ └┘
src             └─────────┘    └────┘  └─────────────┘    └┘
typ     └┘   └─┘└─────────┘  └┘└────┘  └─────────────┘ └┘ └┘
210  
211  /--
212    This is a special-purpose tactic that lifts padic_norm (f (stationary_point f)) to
213    padic_norm (f (max _ _ _)).
214  -/
215  meta def tactic.interactive.padic_index_simp (l : interactive.parse interactive.types.pexpr_list)
id                                                     └───────────────┘ └──────────────────────────┘
src                                                    └───────────────┘ └──────────────────────────┘
typ                                                    └───────────────┘ └──────────────────────────┘
doc                                                    └───────────────┘
216    (at_ : interactive.parse interactive.types.location) : tactic unit :=
id            └───────────────┘ └────────────────────────┘    └────┘ └──┘
src           └───────────────┘ └────────────────────────┘    └────┘ └──┘
typ           └───────────────┘ └────────────────────────┘    └────┘ └──┘
doc           └───────────────┘                                      └──┘
217  do [h, f, g] ← l.mmap tactic.i_to_expr,
id           └───┘ └──────────────┘
src              └───┘ └──────────────┘
typ          └───┘ └──────────────┘
218     index_simp_core h f g at_
id      └─────────────┘       └─┘
src     └─────────────┘
typ     └─────────────┘       └─┘
219  end
220  
221  namespace padic_seq
222  section embedding
223  
224  open cau_seq
225  variables {p : ℕ} [hp : nat.prime p]
id                          └───────┘
src                         └───────┘
typ                         └───────┘
doc                          └───────┘
226  include hp
227  
228  lemma norm_mul (f g : padic_seq p) : (f * g).norm = f.norm * g.norm :=
id                         └───────┘         └──┘   └───┘  └───┘
src                        └───────┘            └──┘    └───┘   └───┘
typ                        └───────┘         └──┘   └───┘  └───┘
doc                        └───────┘             └──┘     └───┘    └───┘
229  if hf : f ≈ 0 then
id   └┘       
src  └┘        
typ  └┘       
230    have hg : f * g ≈ 0, from mul_equiv_zero' _ hf,
id                           └─────────────┘   └┘
src                            └─────────────┘
typ                          └─────────────┘   └┘
231    by simp [hf, hg, norm]
id              └┘  └┘  └──┘
src       └────┘  └┘  └┘└──┘└┘
typ       └────┘└┘└┘└┘└┘└──┘└┘
doc       └────┘  └┘  └┘└──┘└┘
txt       └────┘  └┘  └┘    └┘
par       └────┘  └┘  └┘    └┘
pid             └┘  └┘    
st       └───────────────────┘
232  else if hg : g ≈ 0 then
id        └┘       
src       └┘        
typ       └┘       
233    have hf : f * g ≈ 0, from mul_equiv_zero _ hg,
id                           └────────────┘   └┘
src                            └────────────┘
typ                          └────────────┘   └┘
234    by simp [hf, hg, norm]
id              └┘  └┘  └──┘
src       └────┘  └┘  └┘└──┘└┘
typ       └────┘└┘└┘└┘└┘└──┘└┘
doc       └────┘  └┘  └┘└──┘└┘
txt       └────┘  └┘  └┘    └┘
par       └────┘  └┘  └┘    └┘
pid             └┘  └┘    
st       └───────────────────┘
235  else
236    have hfg : ¬ f * g ≈ 0, by apply mul_not_equiv_zero; assumption,
id     └──┘                        └────────────────┘
src                            └────┘└────────────────┘  └────────┘
typ    └──┘                  └────┘└────────────────┘  └────────┘
doc                               └────┘                    └────────┘
txt                               └────┘                    └────────┘
par                               └────┘                    └────────┘
pid                                    
st                               └───────────────────────────────────┘
237    begin
st     └─────
238      unfold norm,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
239      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
240      padic_index_simp [hfg, hf, hg],
id                         └─┘  └┘  └┘
src      └────────────────┘   └┘  └┘  
typ      └────────────────┘└─┘└┘└┘└┘└┘
doc      └────────────────┘   └┘  └┘  
txt      └────────────────┘   └┘  └┘  
par      └────────────────┘   └┘  └┘  
pid                      └┘   └┘  └┘  
st   ─────────────────────────────────┘└─
241      apply padic_norm.mul
id             └────────────┘
src      └────┘└────────────┘
typ      └────┘└────────────┘
doc      └────┘└────────────┘
txt      └────┘              
par      └────┘              
pid                         
st   ─────────────────────────
242    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
243  
244  lemma eq_zero_iff_equiv_zero (f : padic_seq p) : mk f = 0 ↔ f ≈ 0 :=
id                                     └───────┘     └┘       
src                                    └───────┘      └┘         
typ                                    └───────┘     └┘       
doc                                    └───────┘
245  mk_eq
id   └───┘
src  └───┘
typ  └───┘
246  
247  lemma ne_zero_iff_nequiv_zero (f : padic_seq p) : mk f ≠ 0 ↔ ¬ f ≈ 0 :=
id                                      └───────┘     └┘        
src                                     └───────┘      └┘          
typ                                     └───────┘     └┘        
doc                                     └───────┘
248  not_iff_not.2 (eq_zero_iff_equiv_zero _)
id   └─────────┘   └────────────────────┘
src  └─────────┘   └────────────────────┘
typ  └─────────┘   └────────────────────┘
249  
250  lemma norm_const (q : ℚ) : norm (const (padic_norm p) q) = padic_norm p q :=
id                             └──┘  └───┘  └────────┘      └────────┘  
src                            └──┘  └───┘  └────────┘        └────────┘
typ                            └──┘  └───┘  └────────┘      └────────┘  
doc                            └──┘  └───┘  └────────┘         └────────┘
251  if hq : q = 0 then
id   └┘       
src  └┘        
typ  └┘       
252    have (const (padic_norm p) q) ≈ 0,
id           └───┘  └────────┘     
src          └───┘  └────────┘       
typ          └───┘  └────────┘     
doc          └───┘  └────────┘
253      by simp [hq]; apply setoid.refl (const (padic_norm p) 0),
id                └┘         └─────────┘  └───┘  └────────┘ 
src         └────┘    └────┘└─────────┘ └───┘ └────────┘ └──┘
typ         └────┘└┘  └────┘└─────────┘ └───┘ └────────┘└──┘
doc         └────┘    └────┘            └───┘ └────────┘ └──┘
txt         └────┘    └────┘                             └──┘
par         └────┘    └────┘                             └──┘
pid                                                   └──┘
st         └────────────────────────────────────────────────────┘
254    by subst hq; simp [norm, this]
id              └┘        └──┘  └──┘
src       └────┘    └────┘└──┘└┘    └┘
typ       └────┘└┘  └────┘└──┘└┘└──┘└┘
doc       └────┘    └────┘└──┘└┘    └┘
txt       └────┘    └────┘    └┘    └┘
par       └────┘    └────┘    └┘    └┘
pid                        └┘    
st       └───────────────────────────┘
255  else
256    have ¬ (const (padic_norm p) q) ≈ 0, from not_equiv_zero_const_of_nonzero hq,
id     └──┘   └───┘  └────────┘              └─────────────────────────────┘ └┘
src           └───┘  └────────┘                └─────────────────────────────┘
typ    └──┘   └───┘  └────────┘              └─────────────────────────────┘ └┘
doc            └───┘  └────────┘
257    by simp [norm, this]
id              └──┘  └──┘
src       └────┘└──┘└┘    └─
typ       └────┘└──┘└┘└──┘└─
doc       └────┘└──┘└┘    └─
txt       └────┘    └┘    └─
par       └────┘    └┘    └─
pid               └┘    
st       └──────────────────
258  
src  
typ  
doc  
txt  
par  
pid  
st   
259  lemma norm_image (a : padic_seq p) (ha : ¬ a ≈ 0) :
id                         └───────┘           
src                        └───────┘             
typ                        └───────┘           
doc                        └───────┘
260    (∃ (n : ℤ), a.norm = ↑p ^ (-n)) :=
id              └───┘     
src              └───┘      
typ             └───┘     
doc                 └───┘
261  let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha in
id   └─┘                 └─────────────────────────┘ └┘
src                      └─────────────────────────┘
typ  └─┘                 └─────────────────────────┘ └┘
262  by simpa [hk] using padic_norm.image p hk'
id             └┘        └──────────────┘  └─┘
src     └─────┘  └──────┘└──────────────┘    
typ     └─────┘└┘└──────┘└──────────────┘└─┘
doc     └─────┘  └──────┘└──────────────┘    
txt     └─────┘  └──────┘                    
par     └─────┘  └──────┘                    
pid            └────┘                    
st     └────────────────────────────────────────
263  
src  
typ  
doc  
txt  
par  
pid  
st   
264  lemma norm_one : norm (1 : padic_seq p) = 1 :=
id                    └──┘      └───────┘   
src                   └──┘      └───────┘    
typ                   └──┘      └───────┘   
doc                   └──┘      └───────┘
265  have h1 : ¬ (1 : padic_seq p) ≈ 0, from one_not_equiv_zero _,
id                   └───────┘            └────────────────┘
src                  └───────┘             └────────────────┘
typ                  └───────┘            └────────────────┘
doc                   └───────┘
266  by simp [h1, norm, hp.one_lt]
id            └┘  └──┘
src     └────┘  └┘└──┘└┘         └─
typ     └────┘└┘└┘└──┘└┘└───────┘└─
doc     └────┘  └┘└──┘└┘         └─
txt     └────┘  └┘    └┘         └─
par     └────┘  └┘    └┘         └─
pid           └┘    └┘         
st     └───────────────────────────
267  
src  
typ  
doc  
txt  
par  
pid  
st   
268  private lemma norm_eq_of_equiv_aux {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) (hfg : f ≈ g)
id                                             └───────┘                                    
src                                            └───────┘                                       
typ                                            └───────┘                                    
doc                                            └───────┘
269    (h : padic_norm p (f (stationary_point hf)) ≠ padic_norm p (g (stationary_point hg)))
id          └────────┘     └──────────────┘ └┘    └────────┘     └──────────────┘ └┘
src         └────────┘       └──────────────┘       └────────┘       └──────────────┘
typ         └────────┘     └──────────────┘ └┘    └────────┘     └──────────────┘ └┘
doc         └────────┘       └──────────────┘        └────────┘       └──────────────┘
270    (hgt : padic_norm p (f (stationary_point hf)) > padic_norm p (g (stationary_point hg))) :
id            └────────┘     └──────────────┘ └┘    └────────┘     └──────────────┘ └┘
src           └────────┘       └──────────────┘       └────────┘       └──────────────┘
typ           └────────┘     └──────────────┘ └┘    └────────┘     └──────────────┘ └┘
doc           └────────┘       └──────────────┘        └────────┘       └──────────────┘
271    false :=
id     └───┘
src    └───┘
typ    └───┘
272  begin
st   └─────
273    have hpn : padic_norm p (f (stationary_point hf)) - padic_norm p (g (stationary_point hg)) > 0,
id                                                 └┘    └────────┘     └──────────────┘ └┘   
src    └─────────┘                                └─┘└────────┘    └──────────────┘  └─┘└┘
typ    └─────────┘                             └┘└─┘└────────┘  └──────────────┘└┘└─┘└┘
doc    └─────────┘                                └─┘ └────────┘    └──────────────┘  └─┘ └┘
txt    └─────────┘                                └─┘                                 └─┘ └┘
par    └─────────┘                                └─┘                                 └─┘ └┘
pid    └──────┘└─┘                                └─┘                                 └─┘ 
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
274      from sub_pos_of_lt hgt,
id            └───────────┘ └─┘
src      └───┘└───────────┘
typ      └───┘└───────────┘└─┘
doc      └───┘             
txt      └───┘             
par      └───┘             
pid      └───┘             
st   ─────────────────────────┘└─
275    cases hfg _ hpn with N hN,
id           └─┘   └─┘
src    └────┘   └─┘   └────────┘
typ    └────┘└─┘└─┘└─┘└────────┘
doc    └────┘   └─┘   └────────┘
txt    └────┘   └─┘   └────────┘
par    └────┘   └─┘   └────────┘
pid            └─┘   └────────┘
st   ──────────────────────────┘└─
276    let i := max N (max (stationary_point hf) (stationary_point hg)),
id                    └─┘                   └┘   └──────────────┘ └┘
src    └───────┘     └─┘                   └┘ └──────────────┘  └┘
typ    └───────┘    └─┘                 └┘└┘ └──────────────┘└┘└┘
doc    └───────┘                           └┘ └──────────────┘  └┘
txt    └───────┘                           └┘                   └┘
par    └───────┘                           └┘                   └┘
pid    └───┘└─┘                           └┘                   └┘
st   ─────────────────────────────────────────────────────────────────┘└─
277    have hi : i ≥ N, from le_max_left _ _,
id                        └─────────┘
src    └────────┘    └───┘└─────────┘└──┘
typ    └────────┘  └───┘└─────────┘└──┘
doc    └────────┘     └───┘           └──┘
txt    └────────┘     └───┘           └──┘
par    └────────┘     └───┘           └──┘
pid    └─────┘└─┘     └───┘           └──┘
st   ────────────────┘└────────────────────┘└─
278    have hN' := hN _ hi,
id                 └┘   └┘
src    └──────────┘  └─┘
typ    └──────────┘└┘└─┘└┘
doc    └──────────┘  └─┘
txt    └──────────┘  └─┘
par    └──────────┘  └─┘
pid    └──────┘└─┘  └─┘
st   ────────────────────┘└─
279    padic_index_simp [N, hf, hg] at hN' h hgt,
id                         └┘  └┘
src    └────────────────┘ └┘  └┘  └────────────┘
typ    └────────────────┘└┘└┘└┘└┘└────────────┘
doc    └────────────────┘ └┘  └┘  └────────────┘
txt    └────────────────┘ └┘  └┘  └────────────┘
par    └────────────────┘ └┘  └┘  └────────────┘
pid                    └┘ └┘  └┘  └───────────┘
st   ──────────────────────────────────────────┘└─
280    have hpne : padic_norm p (f i) ≠ padic_norm p (-(g i)),
id                                    └────────┘     
src    └──────────┘              └┘└────────┘     └┘
typ    └──────────┘             └┘└────────┘  └┘
doc    └──────────┘              └┘ └────────┘      └┘
txt    └──────────┘              └┘                 └┘
par    └──────────┘              └┘                 └┘
pid    └───────┘└─┘              └┘                 └┘
st   ───────────────────────────────────────────────────────┘
281      by rwa [ ←padic_norm.neg p (g i)] at h,
id                 └────────────┘    
src         └─────┘└────────────┘    └─────┘
typ         └─────┘└────────────┘ └─────┘
doc         └─────┘└────────────┘    └─────┘
txt         └─────┘                  └─────┘
par         └─────┘                  └─────┘
pid            └──┘                  └┘└───┘
st               └──────────────────────┘     └─
282    let hpnem := add_eq_max_of_ne p hpne,
id                  └──────────────┘  └──┘
src    └───────────┘└──────────────┘ 
typ    └───────────┘└──────────────┘└──┘
doc    └───────────┘└──────────────┘ 
txt    └───────────┘                 
par    └───────────┘                 
pid    └───────┘└─┘                 
st   ─────────────────────────────────────┘└─
283    have hpeq : padic_norm p ((f - g) i) = max (padic_norm p (f i)) (padic_norm p (g i)),
id                                           └─┘                      └────────┘    
src    └──────────┘                └┘ └┘└─┘               └─┘ └────────┘    └┘
typ    └──────────┘                └┘ └┘└─┘              └─┘ └────────┘ └┘
doc    └──────────┘                └┘ └┘                   └─┘ └────────┘    └┘
txt    └──────────┘                └┘ └┘                   └─┘               └┘
par    └──────────┘                └┘ └┘                   └─┘               └┘
pid    └───────┘└─┘                └┘ └┘                   └─┘               └┘
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
284    { rwa padic_norm.neg at hpnem },
id           └────────────┘
src      └──┘└────────────┘└────────┘
typ      └──┘└────────────┘└────────┘
doc      └──┘└────────────┘└────────┘
txt      └──┘              └────────┘
par      └──┘              └────────┘
pid                       └───────┘
st   ───┘└──────────────────────────┘└┘
285    rw [hpeq, max_eq_left_of_lt hgt] at hN',
id         └──┘  └───────────────┘ └─┘
src    └──┘    └┘└───────────────┘   └──────┘
typ    └──┘└──┘└┘└───────────────┘└─┘└──────┘
doc    └──┘    └┘                    └──────┘
txt    └──┘    └┘                    └──────┘
par    └──┘    └┘                    └──────┘
pid      └┘    └┘                    └─────┘
st   ─────────┘└─────────────────────┘└─────┘└─
286    have : padic_norm p (f i) < padic_norm p (f i),
id                                └────────┘    
src    └─────┘              └┘└────────┘    
typ    └─────┘              └┘└────────┘ 
doc    └─────┘              └┘ └────────┘    
txt    └─────┘              └┘               
par    └─────┘              └┘               
pid    └───┘└┘              └┘               
st   ───────────────────────────────────────────────┘└─
287    { apply lt_of_lt_of_le hN', apply sub_le_self, apply padic_norm.nonneg },
id             └────────────┘ └─┘        └─────────┘        └───────────────┘
src      └────┘└────────────┘     └────┘└─────────┘  └────┘└───────────────┘
typ      └────┘└────────────┘└─┘  └────┘└─────────┘  └────┘└───────────────┘
doc      └────┘                   └────┘             └────┘└───────────────┘
txt      └────┘                   └────┘             └────┘                 
par      └────┘                   └────┘             └────┘                 
pid                                                                      
st   ───┘└──────────────────────┘└─────────────────┘└────────────────────────┘└┘
288    exact lt_irrefl _ this
id           └───────┘   └──┘
src    └────┘└───────┘└─┘    
typ    └────┘└───────┘└─┘└──┘
doc    └────┘         └─┘    
txt    └────┘         └─┘    
par    └────┘         └─┘    
pid                  └─┘    
st   ────────────────────────┘
289  end
st   └─┘
290  
291  private lemma norm_eq_of_equiv {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) (hfg : f ≈ g) :
id                                         └───────┘                                    
src                                        └───────┘                                       
typ                                        └───────┘                                    
doc                                        └───────┘
292    padic_norm p (f (stationary_point hf)) = padic_norm p (g (stationary_point hg)) :=
id     └────────┘     └──────────────┘ └┘    └────────┘     └──────────────┘ └┘
src    └────────┘       └──────────────┘       └────────┘       └──────────────┘
typ    └────────┘     └──────────────┘ └┘    └────────┘     └──────────────┘ └┘
doc    └────────┘       └──────────────┘        └────────┘       └──────────────┘
293  begin
st   └─────
294    by_contradiction h,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid                    └┘
st   ───────────────────┘└─
295    cases (decidable.em (padic_norm p (f (stationary_point hf)) >
id            └──────────┘                                   └┘   
src    └────┘ └──────────┘                                 └─┘
typ    └────┘ └──────────┘                              └┘└─┘
doc    └────┘                                              └─┘ 
txt    └────┘                                              └─┘ 
par    └────┘                                              └─┘ 
pid                                                       └─┘ 
st   ────────────────────────────────────────────────────────────────
296            padic_norm p (g (stationary_point hg))))
id             └────────┘     └──────────────┘ └┘
src  ─────────┘└────────┘    └──────────────┘  └────
typ  ─────────┘└────────┘  └──────────────┘└┘└────
doc  ─────────┘└────────┘    └──────────────┘  └────
txt  ─────────┘                                └────
par  ─────────┘                                └────
pid  ─────────┘                                └──┘
st   ───────────────────────────────────────────────────
297        with hgt hngt,
src  ──────────────────┘
typ  ──────────────────┘
doc  ──────────────────┘
txt  ──────────────────┘
par  ──────────────────┘
pid  ──────────────────┘
st   ──────────────────┘└─
298    { exact norm_eq_of_equiv_aux hf hg hfg h hgt },
id             └──────────────────┘ └┘ └┘ └─┘  └─┘
src      └────┘└──────────────────┘           
typ      └────┘└──────────────────┘└┘└┘└─┘└─┘
doc      └────┘                               
txt      └────┘                               
par      └────┘                               
pid                                          
st   ───┘└─────────────────────────────────────────┘└┘
299    { apply norm_eq_of_equiv_aux hg hf (setoid.symm hfg) (ne.symm h),
id             └──────────────────┘ └┘ └┘  └─────────┘ └─┘   └─────┘ 
src      └────┘└──────────────────┘     └─────────┘   └┘ └─────┘ 
typ      └────┘└──────────────────┘└┘└┘ └─────────┘└─┘└┘ └─────┘
doc      └────┘                                       └┘         
txt      └────┘                                       └┘         
par      └────┘                                       └┘         
pid                                                  └┘         
st   ─────────────────────────────────────────────────────────────────┘└─
300      apply lt_of_le_of_ne,
id             └────────────┘
src      └────┘└────────────┘
typ      └────┘└────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────┘└─
301      apply le_of_not_gt hngt,
id             └──────────┘ └──┘
src      └────┘└──────────┘
typ      └────┘└──────────┘└──┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                       
st   ──────────────────────────┘└─
302      apply h }
src      └────┘ 
typ      └────┘ 
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───────────┘└─
303  end
st   ──┘
304  
305  theorem norm_equiv {f g : padic_seq p} (hfg : f ≈ g) : f.norm = g.norm :=
id                             └───────┘                └───┘  └───┘
src                            └───────┘                    └───┘   └───┘
typ                            └───────┘                └───┘  └───┘
doc                            └───────┘                     └───┘    └───┘
306  if hf : f ≈ 0 then
id   └┘       
src  └┘        
typ  └┘       
307    have hg : g ≈ 0, from setoid.trans (setoid.symm hfg) hf,
id                         └──────────┘  └─────────┘ └─┘  └┘
src                         └──────────┘  └─────────┘
typ                        └──────────┘  └─────────┘ └─┘  └┘
308    by simp [norm, hf, hg]
id              └──┘  └┘  └┘
src       └────┘└──┘└┘  └┘  └┘
typ       └────┘└──┘└┘└┘└┘└┘└┘
doc       └────┘└──┘└┘  └┘  └┘
txt       └────┘    └┘  └┘  └┘
par       └────┘    └┘  └┘  └┘
pid               └┘  └┘  
st       └───────────────────┘
309  else have hg : ¬ g ≈ 0, from hf ∘ setoid.trans hfg,
id        └──┘                 └┘  └──────────┘ └─┘
src                                 └──────────┘
typ       └──┘                 └┘  └──────────┘ └─┘
310  by unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg
id                                    └──────────────┘ └┘ └┘ └─┘
src     └─────────┘  └───────┘  └────┘└──────────────┘       
typ     └─────────┘  └───────┘  └────┘└──────────────┘└┘└┘└─┘
doc     └─────────┘  └───────┘  └────┘                       
txt     └─────────┘  └───────┘  └────┘                       
par     └─────────┘  └───────┘  └────┘                       
pid           └───┘                                         
st     └─────────────────────────────────────────────────────────
311  
src  
typ  
doc  
txt  
par  
pid  
st   
312  private lemma norm_nonarchimedean_aux {f g : padic_seq p}
id                                                └───────┘ 
src                                               └───────┘
typ                                               └───────┘ 
doc                                               └───────┘
313    (hfg : ¬ f + g ≈ 0) (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) : (f + g).norm ≤ max (f.norm) (g.norm) :=
id                                                  └──┘   └─┘  └───┘   └───┘
src                                                       └──┘   └─┘   └───┘    └───┘
typ                                                 └──┘   └─┘  └───┘   └───┘
doc                                                               └──┘          └───┘    └───┘
314  begin
st   └─────
315    unfold norm, split_ifs,
src    └─────────┘  └───────┘
typ    └─────────┘  └───────┘
doc    └─────────┘  └───────┘
txt    └─────────┘  └───────┘
par    └─────────┘  └───────┘
pid          └───┘
st   ────────────┘└─────────┘└─
316    padic_index_simp [hfg, hf, hg],
id                       └─┘  └┘  └┘
src    └────────────────┘   └┘  └┘  
typ    └────────────────┘└─┘└┘└┘└┘└┘
doc    └────────────────┘   └┘  └┘  
txt    └────────────────┘   └┘  └┘  
par    └────────────────┘   └┘  └┘  
pid                    └┘   └┘  └┘  
st   ───────────────────────────────┘└─
317    apply padic_norm.nonarchimedean
id           └───────────────────────┘
src    └────┘└───────────────────────┘
typ    └────┘└───────────────────────┘
doc    └────┘└───────────────────────┘
txt    └────┘                         
par    └────┘                         
pid                                  
st   ─────────────────────────────────┘
318  end
st   └─┘
319  
320  theorem norm_nonarchimedean (f g : padic_seq p) : (f + g).norm ≤ max (f.norm) (g.norm) :=
id                                      └───────┘         └──┘   └─┘  └───┘   └───┘
src                                     └───────┘            └──┘   └─┘   └───┘    └───┘
typ                                     └───────┘         └──┘   └─┘  └───┘   └───┘
doc                                     └───────┘             └──┘          └───┘    └───┘
321  if hfg : f + g ≈ 0 then
id   └┘          
src  └┘            
typ  └┘          
322    have 0 ≤ max (f.norm) (g.norm), from le_max_left_of_le (norm_nonneg _),
id             └─┘  └───┘   └───┘        └───────────────┘  └─────────┘
src            └─┘   └───┘    └───┘        └───────────────┘  └─────────┘
typ            └─┘  └───┘   └───┘        └───────────────┘  └─────────┘
doc                   └───┘    └───┘
323    by simpa [hfg, norm]
id               └─┘  └──┘
src       └─────┘   └┘└──┘└┘
typ       └─────┘└─┘└┘└──┘└┘
doc       └─────┘   └┘└──┘└┘
txt       └─────┘   └┘    └┘
par       └─────┘   └┘    └┘
pid               └┘    
st       └─────────────────┘
324  else if hf : f ≈ 0 then
id        └┘       
src       └┘        
typ       └┘       
325    have hfg' : f + g ≈ g,
id                     
src                     
typ                    
326    { change lim_zero (f - 0) at hf,
id              └──────┘   
src      └─────┘└──────┘  └───────┘
typ      └─────┘└──────┘ └───────┘
doc      └─────┘└──────┘   └───────┘
txt      └─────┘           └───────┘
par      └─────┘           └───────┘
pid                       └─┘└───┘
st     └─────────────────────────────┘└─
327      show lim_zero (f + g - g), by simpa using hf },
id            └──────┘                          └┘
src      └───┘└──────┘          └──────────┘  
typ      └───┘└──────┘        └──────────┘└┘
doc      └───┘└──────┘           └──────────┘  
txt      └───┘                   └──────────┘  
par      └───┘                   └──────────┘  
pid      └───┘                        └────┘  
st   ────────────────────────────┘                    └┘
328    have hcfg : (f + g).norm = g.norm, from norm_equiv hfg',
id                     └──┘   └───┘       └────────┘ └──┘
src                      └──┘    └───┘       └────────┘
typ                    └──┘   └───┘       └────────┘ └──┘
doc                       └──┘     └───┘
329    have hcl : f.norm = 0, from (norm_zero_iff f).2 hf,
id                └───┘           └───────────┘    └┘
src                └───┘           └───────────┘   
typ               └───┘           └───────────┘    └┘
doc                └───┘
330    have max (f.norm) (g.norm) = g.norm,
id          └─┘  └───┘   └───┘   └───┘
src         └─┘   └───┘    └───┘    └───┘
typ         └─┘  └───┘   └───┘   └───┘
doc               └───┘    └───┘     └───┘
331      by rw hcl; exact max_eq_right (norm_nonneg _),
id             └─┘        └──────────┘  └─────────┘
src         └─┘     └────┘└──────────┘ └─────────┘└─┘
typ         └─┘└─┘  └────┘└──────────┘ └─────────┘└─┘
doc         └─┘     └────┘                        └─┘
txt         └─┘     └────┘                        └─┘
par         └─┘     └────┘                        └─┘
pid                                             └─┘
st         └─────────────────────────────────────────┘
332    by rw [this, hcfg]
id            └──┘  └──┘
src       └──┘    └┘    └┘
typ       └──┘└──┘└┘└──┘└┘
doc       └──┘    └┘    └┘
txt       └──┘    └┘    └┘
par       └──┘    └┘    └┘
pid         └┘    └┘    
st       └───────┘└────┘
333  else if hg : g ≈ 0 then
id        └┘       
src       └┘        
typ       └┘       
334    have hfg' : f + g ≈ f,
id                     
src                     
typ                    
335    { change lim_zero (g - 0) at hg,
id              └──────┘  
src      └─────┘└──────┘   └───────┘
typ      └─────┘└──────┘  └───────┘
doc      └─────┘└──────┘   └───────┘
txt      └─────┘           └───────┘
par      └─────┘           └───────┘
pid                       └─┘└───┘
st     └─────────────────────────────┘└─
336      show lim_zero (f + g - f), by  simpa [add_sub_cancel'] using hg },
id            └──────┘                       └─────────────┘        └┘
src      └───┘└──────┘            └─────┘└─────────────┘└──────┘  
typ      └───┘└──────┘          └─────┘└─────────────┘└──────┘└┘
doc      └───┘└──────┘            └─────┘               └──────┘  
txt      └───┘                    └─────┘               └──────┘  
par      └───┘                    └─────┘               └──────┘  
pid      └───┘                                        └────┘  
st   ────────────────────────────┘                                       └┘
337    have hcfg : (f + g).norm = f.norm, from norm_equiv hfg',
id                     └──┘   └───┘       └────────┘ └──┘
src                      └──┘    └───┘       └────────┘
typ                    └──┘   └───┘       └────────┘ └──┘
doc                       └──┘     └───┘
338    have hcl : g.norm = 0, from (norm_zero_iff g).2 hg,
id                └───┘           └───────────┘    └┘
src                └───┘           └───────────┘   
typ               └───┘           └───────────┘    └┘
doc                └───┘
339    have max (f.norm) (g.norm) = f.norm,
id          └─┘  └───┘   └───┘   └───┘
src         └─┘   └───┘    └───┘    └───┘
typ         └─┘  └───┘   └───┘   └───┘
doc               └───┘    └───┘     └───┘
340      by rw hcl; exact max_eq_left (norm_nonneg _),
id             └─┘        └─────────┘  └─────────┘
src         └─┘     └────┘└─────────┘ └─────────┘└─┘
typ         └─┘└─┘  └────┘└─────────┘ └─────────┘└─┘
doc         └─┘     └────┘                       └─┘
txt         └─┘     └────┘                       └─┘
par         └─┘     └────┘                       └─┘
pid                                            └─┘
st         └────────────────────────────────────────┘
341    by rw [this, hcfg]
id            └──┘  └──┘
src       └──┘    └┘    └┘
typ       └──┘└──┘└┘└──┘└┘
doc       └──┘    └┘    └┘
txt       └──┘    └┘    └┘
par       └──┘    └┘    └┘
pid         └┘    └┘    
st       └───────┘└────┘
342  else norm_nonarchimedean_aux hfg hf hg
id        └─────────────────────┘ └─┘ └┘ └┘
src       └─────────────────────┘
typ       └─────────────────────┘ └─┘ └┘ └┘
343  
344  lemma norm_eq {f g : padic_seq p} (h : ∀ k, padic_norm p (f k) = padic_norm p (g k)) :
id                        └───────┘            └────────┘       └────────┘    
src                       └───────┘              └────────┘          └────────┘
typ                       └───────┘            └────────┘       └────────┘    
doc                       └───────┘              └────────┘           └────────┘
345    f.norm = g.norm :=
id     └───┘  └───┘
src     └───┘   └───┘
typ    └───┘  └───┘
doc     └───┘    └───┘
346  if hf : f ≈ 0 then
id   └┘       
src  └┘        
typ  └┘       
347    have hg : g ≈ 0, from equiv_zero_of_val_eq_of_equiv_zero h hf,
id                         └────────────────────────────────┘  └┘
src                         └────────────────────────────────┘
typ                        └────────────────────────────────┘  └┘
348    by simp [hf, hg, norm]
id              └┘  └┘  └──┘
src       └────┘  └┘  └┘└──┘└┘
typ       └────┘└┘└┘└┘└┘└──┘└┘
doc       └────┘  └┘  └┘└──┘└┘
txt       └────┘  └┘  └┘    └┘
par       └────┘  └┘  └┘    └┘
pid             └┘  └┘    
st       └───────────────────┘
349  else
350    have hg : ¬ g ≈ 0, from λ hg, hf $ equiv_zero_of_val_eq_of_equiv_zero (by simp [h]) hg,
id     └──┘                   └┘  └┘   └────────────────────────────────┘              └┘
src                                     └────────────────────────────────┘     └────┘ 
typ    └──┘                   └┘  └┘   └────────────────────────────────┘     └────┘  └┘
doc                                                                              └────┘ 
txt                                                                              └────┘ 
par                                                                              └────┘ 
pid                                                                                   
st                                                                              └───────┘
351    begin
st     └─────
352      simp [hg, hf, norm],
id             └┘  └┘  └──┘
src      └────┘  └┘  └┘└──┘
typ      └────┘└┘└┘└┘└┘└──┘
doc      └────┘  └┘  └┘└──┘
txt      └────┘  └┘  └┘    
par      └────┘  └┘  └┘    
pid            └┘  └┘    
st   ──────────────────────┘└─
353      let i := max (stationary_point hf) (stationary_point hg),
id                └─┘                   └┘   └──────────────┘ └┘
src      └───────┘└─┘                   └┘ └──────────────┘  
typ      └───────┘└─┘                 └┘└┘ └──────────────┘└┘
doc      └───────┘                      └┘ └──────────────┘  
txt      └───────┘                      └┘                   
par      └───────┘                      └┘                   
pid      └───┘└─┘                      └┘                   
st   ───────────────────────────────────────────────────────────┘└─
354      have hpf : padic_norm p (f (stationary_point hf)) = padic_norm p (f i),
id                                   └──────────────┘ └┘    └────────┘    
src      └─────────┘              └──────────────┘  └─┘└────────┘    
typ      └─────────┘              └──────────────┘└┘└─┘└────────┘ 
doc      └─────────┘              └──────────────┘  └─┘ └────────┘    
txt      └─────────┘                                └─┘               
par      └─────────┘                                └─┘               
pid      └──────┘└─┘                                └─┘               
st   ─────────────────────────────────────────────────────────────────────────┘└─
355      { apply stationary_point_spec, apply le_max_left, apply le_refl },
id               └───────────────────┘        └─────────┘        └─────┘
src        └────┘└───────────────────┘  └────┘└─────────┘  └────┘└─────┘
typ        └────┘└───────────────────┘  └────┘└─────────┘  └────┘└─────┘
doc        └────┘                       └────┘             └────┘       
txt        └────┘                       └────┘             └────┘       
par        └────┘                       └────┘             └────┘       
pid                                                                  
st   ─────┘└─────────────────────────┘└─────────────────┘└──────────────┘└┘
356      have hpg : padic_norm p (g (stationary_point hg)) = padic_norm p (g i),
id                                   └──────────────┘ └┘     └────────┘    
src      └─────────┘              └──────────────┘  └─┘ └────────┘    
typ      └─────────┘              └──────────────┘└┘└─┘ └────────┘ 
doc      └─────────┘              └──────────────┘  └─┘ └────────┘    
txt      └─────────┘                                └─┘               
par      └─────────┘                                └─┘               
pid      └──────┘└─┘                                └─┘               
st   ─────────────────────────────────────────────────────────────────────────┘└─
357      { apply stationary_point_spec, apply le_max_right, apply le_refl },
id               └───────────────────┘        └──────────┘        └─────┘
src        └────┘└───────────────────┘  └────┘└──────────┘  └────┘└─────┘
typ        └────┘└───────────────────┘  └────┘└──────────┘  └────┘└─────┘
doc        └────┘                       └────┘              └────┘       
txt        └────┘                       └────┘              └────┘       
par        └────┘                       └────┘              └────┘       
pid                                                                   
st   ─────┘└─────────────────────────┘└──────────────────┘└──────────────┘└┘
358      rw [hpf, hpg, h]
id           └─┘  └─┘  
src      └──┘   └┘   └┘ └─
typ      └──┘└─┘└┘└─┘└┘└─
doc      └──┘   └┘   └┘ └─
txt      └──┘   └┘   └┘ └─
par      └──┘   └┘   └┘ └─
pid        └┘   └┘   └┘ 
st   ──────────┘└───┘└─┘
359    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
360  
361  lemma norm_neg (a : padic_seq p) : (-a).norm = a.norm :=
id                       └───────┘       └──┘   └───┘
src                      └───────┘         └──┘    └───┘
typ                      └───────┘       └──┘   └───┘
doc                      └───────┘          └──┘     └───┘
362  norm_eq $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
363  
src  
typ  
doc  
txt  
par  
pid  
st   
364  lemma norm_eq_of_add_equiv_zero {f g : padic_seq p} (h : f + g ≈ 0) : f.norm = g.norm :=
id                                          └───────┘                 └───┘  └───┘
src                                         └───────┘                     └───┘   └───┘
typ                                         └───────┘                 └───┘  └───┘
doc                                         └───────┘                       └───┘    └───┘
365  have lim_zero (f + g - 0), from h,
id        └──────┘               
src       └──────┘       
typ       └──────┘               
doc       └──────┘
366  have f ≈ -g, from show lim_zero (f - (-g)), by simpa,
id                      └──────┘     
src                       └──────┘              └───┘
typ                     └──────┘            └───┘
doc                         └──────┘                └───┘
txt                                                 └───┘
par                                                 └───┘
st                                                 └────┘
367  have f.norm = (-g).norm, from norm_equiv this,
id        └───┘    └──┘        └────────┘ └──┘
src        └───┘     └──┘        └────────┘
typ       └───┘    └──┘        └────────┘ └──┘
doc        └───┘       └──┘
368  by simpa [norm_neg] using this
id             └──────┘        └──┘
src     └─────┘└──────┘└──────┘    
typ     └─────┘└──────┘└──────┘└──┘
doc     └─────┘        └──────┘    
txt     └─────┘        └──────┘    
par     └─────┘        └──────┘    
pid                  └────┘    
st     └────────────────────────────
369  
src  
typ  
doc  
txt  
par  
pid  
st   
370  lemma add_eq_max_of_ne {f g : padic_seq p} (hfgne : f.norm ≠ g.norm) :
id                                 └───────┘            └───┘  └───┘
src                                └───────┘              └───┘   └───┘
typ                                └───────┘            └───┘  └───┘
doc                                └───────┘              └───┘    └───┘
371    (f + g).norm = max f.norm g.norm :=
id         └──┘   └─┘ └───┘ └───┘
src          └──┘   └─┘  └───┘  └───┘
typ        └──┘   └─┘ └───┘ └───┘
doc           └──┘         └───┘  └───┘
372  have hfg : ¬f + g ≈ 0, from mt norm_eq_of_add_equiv_zero hfgne,
id                          └┘ └───────────────────────┘ └───┘
src                           └┘ └───────────────────────┘
typ                         └┘ └───────────────────────┘ └───┘
373  if hf : f ≈ 0 then
id   └┘       
src  └┘        
typ  └┘       
374    have lim_zero (f - 0), from hf,
id          └──────┘             └┘
src         └──────┘    
typ         └──────┘             └┘
doc         └──────┘
375    have f + g ≈ g, from show lim_zero ((f + g) - g), by simpa,
id                          └──────┘        
src                            └──────┘                 └───┘
typ                         └──────┘              └───┘
doc                              └──────┘                   └───┘
txt                                                         └───┘
par                                                         └───┘
st                                                         └────┘
376    have h1 : (f+g).norm = g.norm, from norm_equiv this,
id                 └──┘   └───┘       └────────┘ └──┘
src                  └──┘    └───┘       └────────┘
typ                └──┘   └───┘       └────────┘ └──┘
doc                   └──┘     └───┘
377    have h2 : f.norm = 0, from (norm_zero_iff _).2 hf,
id               └───┘           └───────────┘     └┘
src               └───┘           └───────────┘   
typ              └───┘           └───────────┘     └┘
doc               └───┘
378    by rw [h1, h2]; rw max_eq_right (norm_nonneg _)
id            └┘  └┘      └──────────┘  └─────────┘
src       └──┘  └┘    └─┘└──────────┘ └─────────┘└──┘
typ       └──┘└┘└┘└┘  └─┘└──────────┘ └─────────┘└──┘
doc       └──┘  └┘    └─┘                        └──┘
txt       └──┘  └┘    └─┘                        └──┘
par       └──┘  └┘    └─┘                        └──┘
pid         └┘  └┘                              └─┘
st       └─────┘└──┘└───┘└──────────┘└───────────────┘
379  else if hg : g ≈ 0 then
id        └┘       
src       └┘        
typ       └┘       
380    have lim_zero (g - 0), from hg,
id          └──────┘             └┘
src         └──────┘    
typ         └──────┘             └┘
doc         └──────┘
381    have f + g ≈ f, from show lim_zero ((f + g) - f), by rw [add_sub_cancel']; simpa,
id                          └──────┘                  └─────────────┘
src                            └──────┘                 └──┘└─────────────┘  └───┘
typ                         └──────┘              └──┘└─────────────┘  └───┘
doc                              └──────┘                   └──┘                 └───┘
txt                                                         └──┘                 └───┘
par                                                         └──┘                 └───┘
pid                                                           └┘               
st                                                         └──────────────────┘└─────┘
382    have h1 : (f+g).norm = f.norm, from norm_equiv this,
id                 └──┘   └───┘       └────────┘ └──┘
src                  └──┘    └───┘       └────────┘
typ                └──┘   └───┘       └────────┘ └──┘
doc                   └──┘     └───┘
383    have h2 : g.norm = 0, from (norm_zero_iff _).2 hg,
id               └───┘           └───────────┘     └┘
src               └───┘           └───────────┘   
typ              └───┘           └───────────┘     └┘
doc               └───┘
384    by rw [h1, h2]; rw max_eq_left (norm_nonneg _)
id            └┘  └┘      └─────────┘  └─────────┘
src       └──┘  └┘    └─┘└─────────┘ └─────────┘└──┘
typ       └──┘└┘└┘└┘  └─┘└─────────┘ └─────────┘└──┘
doc       └──┘  └┘    └─┘                       └──┘
txt       └──┘  └┘    └─┘                       └──┘
par       └──┘  └┘    └─┘                       └──┘
pid         └┘  └┘                             └─┘
st       └─────┘└──┘└───┘└─────────┘└───────────────┘
385  else
386  begin
st   └─────
387    unfold norm at ⊢ hfgne, split_ifs at ⊢ hfgne,
src    └────────────────────┘  └──────────────────┘
typ    └────────────────────┘  └──────────────────┘
doc    └────────────────────┘  └──────────────────┘
txt    └────────────────────┘  └──────────────────┘
par    └────────────────────┘  └──────────────────┘
pid          └───┘└─────────┘           └─────────┘
st   ───────────────────────┘└────────────────────┘└─
388    padic_index_simp [hfg, hf, hg] at ⊢ hfgne,
id                       └─┘  └┘  └┘
src    └────────────────┘   └┘  └┘  └──────────┘
typ    └────────────────┘└─┘└┘└┘└┘└┘└──────────┘
doc    └────────────────┘   └┘  └┘  └──────────┘
txt    └────────────────┘   └┘  └┘  └──────────┘
par    └────────────────┘   └┘  └┘  └──────────┘
pid                    └┘   └┘  └┘  └─────────┘
st   ──────────────────────────────────────────┘└─
389    apply padic_norm.add_eq_max_of_ne,
id           └─────────────────────────┘
src    └────┘└─────────────────────────┘
typ    └────┘└─────────────────────────┘
doc    └────┘└─────────────────────────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────────────┘└─
390    simpa [hf, hg, norm] using hfgne
id            └┘  └┘  └──┘        └───┘
src    └─────┘  └┘  └┘└──┘└──────┘     
typ    └─────┘└┘└┘└┘└┘└──┘└──────┘└───┘
doc    └─────┘  └┘  └┘└──┘└──────┘     
txt    └─────┘  └┘  └┘    └──────┘     
par    └─────┘  └┘  └┘    └──────┘     
pid           └┘  └┘    └────┘     
st   ──────────────────────────────────┘
391  end
id   └─┘
typ  └─┘
st   └─┘
392  
393  end embedding
394  end padic_seq
395  
396  /-- The p-adic numbers `Q_[p]` are the Cauchy completion of `ℚ` with respect to the p-adic norm. -/
397  def padic (p : ℕ) [nat.prime p] := @cau_seq.completion.Cauchy _ _ _ _ (padic_norm p) _
id                     └───────┘       └───────────────────────┘          └────────┘ 
src                    └───────┘        └───────────────────────┘          └────────┘
typ                    └───────┘       └───────────────────────┘          └────────┘ 
doc                     └───────┘                                           └────────┘
398  notation `ℚ_[` p `]` := padic p
id                           └───┘
src                          └───┘
typ                          └───┘
doc                          └───┘
399  
400  namespace padic
401  
402  section completion
403  variables {p : ℕ} [nat.prime p]
id                     └───────┘
src                    └───────┘
typ                    └───────┘
doc                     └───────┘
404  
405  /-- The discrete field structure on ℚ_p is inherited from the Cauchy completion construction. -/
406  instance discrete_field : discrete_field (ℚ_[p]) :=
id                             └────────────┘  └─┘
src                            └────────────┘  └─┘ 
typ                            └────────────┘  └─┘
doc                                            └─┘ 
407  cau_seq.completion.discrete_field
id   └───────────────────────────────┘
src  └───────────────────────────────┘
typ  └───────────────────────────────┘
408  
409  instance : inhabited ℚ_[p] := ⟨0⟩
id              └───────┘ └─┘
src             └───────┘ └─┘ 
typ             └───────┘ └─┘
doc                       └─┘ 
410  
411  -- short circuits
412  
413  instance : has_zero ℚ_[p] := by apply_instance
id              └──────┘ └─┘
src             └──────┘ └─┘        └─────────────┘
typ             └──────┘ └─┘       └─────────────┘
doc                      └─┘        └─────────────┘
txt                                  └─────────────┘
par                                  └─────────────┘
pid                                                
st                                  └──────────────┘
414  instance : has_one ℚ_[p] := by apply_instance
id              └─────┘ └─┘
src             └─────┘ └─┘        └─────────────┘
typ             └─────┘ └─┘       └─────────────┘
doc                     └─┘        └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
415  instance : has_add ℚ_[p] := by apply_instance
id              └─────┘ └─┘
src             └─────┘ └─┘        └─────────────┘
typ             └─────┘ └─┘       └─────────────┘
doc                     └─┘        └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
416  instance : has_mul ℚ_[p] := by apply_instance
id              └─────┘ └─┘
src             └─────┘ └─┘        └─────────────┘
typ             └─────┘ └─┘       └─────────────┘
doc                     └─┘        └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
417  instance : has_sub ℚ_[p] := by apply_instance
id              └─────┘ └─┘
src             └─────┘ └─┘        └─────────────┘
typ             └─────┘ └─┘       └─────────────┘
doc                     └─┘        └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
418  instance : has_neg ℚ_[p] := by apply_instance
id              └─────┘ └─┘
src             └─────┘ └─┘        └─────────────┘
typ             └─────┘ └─┘       └─────────────┘
doc                     └─┘        └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
419  instance : has_div ℚ_[p] := by apply_instance
id              └─────┘ └─┘
src             └─────┘ └─┘        └─────────────┘
typ             └─────┘ └─┘       └─────────────┘
doc                     └─┘        └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
420  instance : add_comm_group ℚ_[p] := by apply_instance
id              └────────────┘ └─┘
src             └────────────┘ └─┘        └─────────────┘
typ             └────────────┘ └─┘       └─────────────┘
doc                            └─┘        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
421  instance : comm_ring ℚ_[p] := by apply_instance
id              └───────┘ └─┘
src             └───────┘ └─┘        └──────────────
typ             └───────┘ └─┘       └──────────────
doc                       └─┘        └──────────────
txt                                   └──────────────
par                                   └──────────────
pid                                                 
st                                   └───────────────
422  
src  
typ  
doc  
txt  
par  
pid  
st   
423  /-- Builds the equivalence class of a Cauchy sequence of rationals. -/
424  def mk : padic_seq p → ℚ_[p] := quotient.mk
id            └───────┘    └─┘    └─────────┘
src           └───────┘     └─┘     └─────────┘
typ           └───────┘    └─┘    └─────────┘
doc           └───────┘     └─┘ 
425  end completion
426  
427  section completion
428  variables (p : ℕ) [nat.prime p]
id                     └───────┘
src                    └───────┘
typ                    └───────┘
doc                     └───────┘
429  
430  lemma mk_eq {f g : padic_seq p} : mk f = mk g ↔ f ≈ g := quotient.eq
id                      └───────┘     └┘   └┘         └─────────┘
src                     └───────┘      └┘    └┘            └─────────┘
typ                     └───────┘     └┘   └┘         └─────────┘
doc                     └───────┘      └┘     └┘
431  
432  /-- Embeds the rational numbers in the p-adic numbers. -/
433  def of_rat : ℚ → ℚ_[p] := cau_seq.completion.of_rat
id                   └─┘    └───────────────────────┘
src                  └─┘     └───────────────────────┘
typ                  └─┘    └───────────────────────┘
doc                  └─┘ 
434  
435  @[simp] lemma of_rat_add : ∀ (x y : ℚ), of_rat p (x + y) = of_rat p x + of_rat p y :=
id                                          └────┘        └────┘    └────┘  
src                                         └────┘           └────┘      └────┘
typ                                         └────┘        └────┘    └────┘  
doc    └──┘                                 └────┘             └────┘       └────┘
436  cau_seq.completion.of_rat_add
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
437  
438  @[simp] lemma of_rat_neg : ∀ (x : ℚ), of_rat p (-x) = -of_rat p x :=
id                                        └────┘      └────┘  
src                                       └────┘        └────┘
typ                                       └────┘      └────┘  
doc    └──┘                               └────┘           └────┘
439  cau_seq.completion.of_rat_neg
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
440  
441  @[simp] lemma of_rat_mul : ∀ (x y : ℚ), of_rat p (x * y) = of_rat p x * of_rat p y :=
id                                          └────┘        └────┘    └────┘  
src                                         └────┘           └────┘      └────┘
typ                                         └────┘        └────┘    └────┘  
doc    └──┘                                 └────┘             └────┘       └────┘
442  cau_seq.completion.of_rat_mul
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
443  
444  @[simp] lemma of_rat_sub : ∀ (x y : ℚ), of_rat p (x - y) = of_rat p x - of_rat p y :=
id                                          └────┘        └────┘    └────┘  
src                                         └────┘           └────┘      └────┘
typ                                         └────┘        └────┘    └────┘  
doc    └──┘                                 └────┘             └────┘       └────┘
445  cau_seq.completion.of_rat_sub
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
446  
447  @[simp] lemma of_rat_div : ∀ (x y : ℚ), of_rat p (x / y) = of_rat p x / of_rat p y :=
id                                          └────┘        └────┘    └────┘  
src                                         └────┘           └────┘      └────┘
typ                                         └────┘        └────┘    └────┘  
doc    └──┘                                 └────┘             └────┘       └────┘
448  cau_seq.completion.of_rat_div
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
449  
450  @[simp] lemma of_rat_one : of_rat p 1 = 1 := rfl
id                              └────┘          └─┘
src                             └────┘           └─┘
typ                             └────┘          └─┘
doc    └──┘                     └────┘
451  
452  @[simp] lemma of_rat_zero : of_rat p 0 = 0 := rfl
id                               └────┘          └─┘
src                              └────┘           └─┘
typ                              └────┘          └─┘
doc    └──┘                      └────┘
453  
454  @[simp] lemma cast_eq_of_rat_of_nat (n : ℕ) : (↑n : ℚ_[p]) = of_rat p n :=
id                                                    └─┘   └────┘  
src                                                    └─┘    └────┘
typ                                                   └─┘   └────┘  
doc    └──┘                                              └─┘     └────┘
455  begin
st   └─────
456    induction n with n ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
457    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
458    { simpa using ih }
id                   └┘
src      └──────────┘  
typ      └──────────┘└┘
doc      └──────────┘  
txt      └──────────┘  
par      └──────────┘  
pid           └────┘  
st   ──────────────────┘└─
459  end
st   ──┘
460  
461  -- without short circuits, this needs an increase of class.instance_max_depth
462  @[simp] lemma cast_eq_of_rat_of_int (n : ℤ) : ↑n = of_rat p n :=
id                                                  └────┘  
src                                                  └────┘
typ                                                 └────┘  
doc    └──┘                                             └────┘
463  by induction n; simp
id                
src     └────────┘   └────
typ     └────────┘  └────
doc     └────────┘   └────
txt     └────────┘   └────
par     └────────┘   └────
pid                     
st     └──────────────────
464  
src  
typ  
doc  
txt  
par  
pid  
st   
465  lemma cast_eq_of_rat : ∀ (q : ℚ), (↑q : ℚ_[p]) = of_rat p q
id                                       └─┘   └────┘  
src                                        └─┘    └────┘
typ                                      └─┘   └────┘  
doc                                         └─┘     └────┘
466  | ⟨n, d, h1, h2⟩ :=
id          └┘  └┘
typ         └┘  └┘
467    show ↑n / ↑d = _, from
id               
src              
typ              
468      have (⟨n, d, h1, h2⟩ : ℚ) = rat.mk n d, from rat.num_denom',
id                                 └────┘           └────────────┘
src                                └────┘           └────────────┘
typ                                └────┘           └────────────┘
doc                                 └────┘
469      by simp [this, rat.mk_eq_div, of_rat_div]
id                └──┘  └───────────┘  └────────┘
src         └────┘    └┘└───────────┘└┘└────────┘└─
typ         └────┘└──┘└┘└───────────┘└┘└────────┘└─
doc         └────┘    └┘             └┘          └─
txt         └────┘    └┘             └┘          └─
par         └────┘    └┘             └┘          └─
pid                 └┘             └┘          
st         └───────────────────────────────────────
470  
src  
typ  
doc  
txt  
par  
pid  
st   
471  @[move_cast] lemma coe_add : ∀ {x y : ℚ}, (↑(x + y) : ℚ_[p]) = ↑x + ↑y := by simp [cast_eq_of_rat]
id                                                    └─┘                  └────────────┘
src                                                     └─┘               └────┘└────────────┘└┘
typ                                                   └─┘            └────┘└────────────┘└┘
doc    └───────┘                                          └─┘                   └────┘              └┘
txt                                                                               └────┘              └┘
par                                                                               └────┘              └┘
pid                                                                                                 
st                                                                               └─────────────────────┘
472  @[move_cast] lemma coe_neg : ∀ {x : ℚ}, (↑(-x) : ℚ_[p]) = -↑x := by simp [cast_eq_of_rat]
id                                                └─┘                └────────────┘
src                                                └─┘            └────┘└────────────┘└┘
typ                                               └─┘          └────┘└────────────┘└┘
doc    └───────┘                                     └─┘               └────┘              └┘
txt                                                                      └────┘              └┘
par                                                                      └────┘              └┘
pid                                                                                        
st                                                                      └─────────────────────┘
473  @[move_cast] lemma coe_mul : ∀ {x y : ℚ}, (↑(x * y) : ℚ_[p]) = ↑x * ↑y := by simp [cast_eq_of_rat]
id                                                    └─┘                  └────────────┘
src                                                     └─┘               └────┘└────────────┘└┘
typ                                                   └─┘            └────┘└────────────┘└┘
doc    └───────┘                                          └─┘                   └────┘              └┘
txt                                                                               └────┘              └┘
par                                                                               └────┘              └┘
pid                                                                                                 
st                                                                               └─────────────────────┘
474  @[move_cast] lemma coe_sub : ∀ {x y : ℚ}, (↑(x - y) : ℚ_[p]) = ↑x - ↑y := by simp [cast_eq_of_rat]
id                                                    └─┘                  └────────────┘
src                                                     └─┘               └────┘└────────────┘└┘
typ                                                   └─┘            └────┘└────────────┘└┘
doc    └───────┘                                          └─┘                   └────┘              └┘
txt                                                                               └────┘              └┘
par                                                                               └────┘              └┘
pid                                                                                                 
st                                                                               └─────────────────────┘
475  @[move_cast] lemma coe_div : ∀ {x y : ℚ}, (↑(x / y) : ℚ_[p]) = ↑x / ↑y := by simp [cast_eq_of_rat]
id                                                    └─┘                  └────────────┘
src                                                     └─┘               └────┘└────────────┘└─
typ                                                   └─┘            └────┘└────────────┘└─
doc    └───────┘                                          └─┘                   └────┘              └─
txt                                                                               └────┘              └─
par                                                                               └────┘              └─
pid                                                                                                 
st                                                                               └──────────────────────
476  
src  
typ  
doc  
txt  
par  
pid  
st   
477  @[squash_cast] lemma coe_one : (↑1 : ℚ_[p]) = 1 := rfl
id                                       └─┘        └─┘
src                                      └─┘         └─┘
typ                                      └─┘        └─┘
doc    └─────────┘                        └─┘ 
478  @[squash_cast] lemma coe_zero : (↑0 : ℚ_[p]) = 0 := rfl
id                                        └─┘        └─┘
src                                       └─┘         └─┘
typ                                       └─┘        └─┘
doc    └─────────┘                         └─┘ 
479  
480  lemma const_equiv {q r : ℚ} : const (padic_norm p) q ≈ const (padic_norm p) r ↔ q = r :=
id                                └───┘  └────────┘     └───┘  └────────┘       
src                               └───┘  └────────┘       └───┘  └────────┘         
typ                               └───┘  └────────┘     └───┘  └────────┘       
doc                               └───┘  └────────┘        └───┘  └────────┘
481  ⟨ λ heq : lim_zero (const (padic_norm p) (q - r)),
id             └──────┘  └───┘  └────────┘      
src            └──────┘  └───┘  └────────┘       
typ            └──────┘  └───┘  └────────┘      
doc            └──────┘  └───┘  └────────┘
482      eq_of_sub_eq_zero $ const_lim_zero.1 heq,
id       └───────────────┘   └────────────┘  └─┘
src      └───────────────┘   └────────────┘  └─┘
typ      └───────────────┘   └────────────┘  └─┘
483    λ heq, by rw heq; apply setoid.refl _ ⟩
id       └─┘        └─┘        └─────────┘
src      └─┘     └─┘└─┘  └────┘└─────────┘└─┘
typ      └─┘     └─┘└─┘  └────┘└─────────┘└─┘
doc              └─┘     └────┘           └─┘
txt              └─┘     └────┘           └─┘
par              └─┘     └────┘           └─┘
pid                                     └┘
st              └───────────────────────────┘
484  
485  lemma of_rat_eq {q r : ℚ} : of_rat p q = of_rat p r ↔ q = r :=
id                              └────┘    └────┘      
src                             └────┘      └────┘        
typ                             └────┘    └────┘      
doc                             └────┘       └────┘
486  ⟨(const_equiv p).1 ∘ quotient.eq.1, λ h, by rw h⟩
id     └─────────┘     └─────────┘             
src    └─────────┘      └─────────┘           └─┘
typ    └─────────┘     └─────────┘          └─┘
doc                                              └─┘
txt                                              └─┘
par                                              └─┘
pid                                                
st                                              └───┘
487  
488  @[elim_cast] lemma coe_inj {q r : ℚ} : (↑q : ℚ_[p]) = ↑r ↔ q = r :=
id                                             └─┘       
src                                             └─┘         
typ                                            └─┘       
doc    └───────┘                                 └─┘ 
489  by simp [cast_eq_of_rat, of_rat_eq]
id            └────────────┘  └───────┘
src     └────┘└────────────┘└┘└───────┘└─
typ     └────┘└────────────┘└┘└───────┘└─
doc     └────┘              └┘         └─
txt     └────┘              └┘         └─
par     └────┘              └┘         └─
pid                       └┘         
st     └─────────────────────────────────
490  
src  
typ  
doc  
txt  
par  
pid  
st   
491  instance : char_zero ℚ_[p] :=
id              └───────┘ └─┘
src             └───────┘ └─┘ 
typ             └───────┘ └─┘
doc             └───────┘ └─┘ 
492  ⟨λ m n, by { rw ← rat.cast_coe_nat, norm_cast, exact id }⟩
id                   └──────────────┘                   └┘
src               └───┘└──────────────┘  └───────┘  └────┘└┘
typ             └───┘└──────────────┘  └───────┘  └────┘└┘
doc               └───┘                  └───────┘  └────┘  
txt               └───┘                  └───────┘  └────┘  
par               └───┘                  └───────┘  └────┘  
pid                 └─┘                                    
st             └──────────────────────┘└─────────┘└─────────┘└┘
493  
494  end completion
495  end padic
496  
497  /-- The rational-valued p-adic norm on ℚ_p is lifted from the norm on Cauchy sequences. The
498  canonical form of this function is the normed space instance, with notation `∥ ∥`. -/
499  def padic_norm_e {p : ℕ} [hp : nat.prime p] : ℚ_[p] → ℚ :=
id                                 └───────┘     └─┘   
src                                └───────┘      └─┘    
typ                                └───────┘     └─┘   
doc                                 └───────┘      └─┘    
500  quotient.lift padic_seq.norm $ @padic_seq.norm_equiv _ _
id   └───────────┘ └────────────┘    └──────────────────┘
src  └───────────┘ └────────────┘    └──────────────────┘
typ  └───────────┘ └────────────┘    └──────────────────┘
doc                └────────────┘
501  
502  namespace padic_norm_e
503  section embedding
504  open padic_seq
505  variables {p : ℕ} [nat.prime p]
id                     └───────┘
src                    └───────┘
typ                    └───────┘
doc                     └───────┘
506  
507  lemma defn (f : padic_seq p) {ε : ℚ} (hε : ε > 0) : ∃ N, ∀ i ≥ N, padic_norm_e (⟦f⟧ - f i) < ε :=
id                   └───────┘                                └──────────┘        
src                  └───────┘                                     └──────────┘          
typ                  └───────┘                                └──────────┘        
doc                  └───────┘                                        └──────────┘
508  begin
st   └─────
509    simp only [padic.cast_eq_of_rat],
id                └──────────────────┘
src    └─────────┘└──────────────────┘
typ    └─────────┘└──────────────────┘
doc    └─────────┘                    
txt    └─────────┘                    
par    └─────────┘                    
pid        └──┘└┘                    
st   ─────────────────────────────────┘└─
510    change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε,
id                            └───┘               
src    └─────┘└┘ └───┘    └───┘└─┘   └──────┘
typ    └─────┘└┘ └───┘    └───┘└─┘  └──────┘
doc    └─────┘ └┘  └───┘     └───┘└─┘   └──────┘ 
txt    └─────┘ └┘  └───┘          └─┘   └──────┘ 
par    └─────┘ └┘  └───┘          └─┘   └──────┘ 
pid           └┘  └───┘          └─┘   └──────┘ 
st   ──────────────────────────────────────────────────┘└─
511    by_contradiction h,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid                    └┘
st   ───────────────────┘└─
512    cases cauchy₂ f hε with N hN,
id           └─────┘  └┘
src    └────┘└─────┘   └────────┘
typ    └────┘└─────┘└┘└────────┘
doc    └────┘          └────────┘
txt    └────┘          └────────┘
par    └────┘          └────────┘
pid                   └────────┘
st   ─────────────────────────────┘└─
513    have : ∀ N, ∃ i ≥ N, (f - const _ (f i)).norm ≥ ε,
id                             └───┘                
src    └─────┘ └┘ └───┘    └───┘└─┘   └──────┘ 
typ    └─────┘ └┘ └───┘    └───┘└─┘  └──────┘ 
doc    └─────┘ └┘  └───┘     └───┘└─┘   └──────┘ 
txt    └─────┘ └┘  └───┘          └─┘   └──────┘ 
par    └─────┘ └┘  └───┘          └─┘   └──────┘ 
pid    └───┘└┘ └┘  └───┘          └─┘   └──────┘ 
st   ──────────────────────────────────────────────────┘
514      by simpa [not_forall] using h,
id                 └────────┘        
src         └─────┘└────────┘└──────┘
typ         └─────┘└────────┘└──────┘
doc         └─────┘          └──────┘
txt         └─────┘          └──────┘
par         └─────┘          └──────┘
pid                        └────┘
st                                    └─
515    rcases this N with ⟨i, hi, hge⟩,
id            └──┘ 
src    └─────┘     └────────────────┘
typ    └─────┘└──┘└────────────────┘
doc    └─────┘     └────────────────┘
txt    └─────┘     └────────────────┘
par    └─────┘     └────────────────┘
pid               └────────────────┘
st   ────────────────────────────────┘└─
516    have hne : ¬ (f - const (padic_norm p) (f i)) ≈ 0,
id                       └───┘  └────────┘        
src    └─────────┘    └───┘ └────────┘ └┘   └─┘└┘
typ    └─────────┘    └───┘ └────────┘└┘ └─┘└┘
doc    └─────────┘    └───┘ └────────┘ └┘   └─┘ └┘
txt    └─────────┘                     └┘   └─┘ └┘
par    └─────────┘                     └┘   └─┘ └┘
pid    └──────┘└─┘                     └┘   └─┘ 
st   ──────────────────────────────────────────────────┘└─
517    { intro h, unfold padic_seq.norm at hge; split_ifs at hge, exact not_lt_of_ge hge hε },
id                                                                      └──────────┘ └─┘ └┘
src      └─────┘  └──────────────────────────┘  └──────────────┘  └────┘└──────────┘     
typ      └─────┘  └──────────────────────────┘  └──────────────┘  └────┘└──────────┘└─┘└┘
doc      └─────┘  └──────────────────────────┘  └──────────────┘  └────┘                 
txt      └─────┘  └──────────────────────────┘  └──────────────┘  └────┘                 
par      └─────┘  └──────────────────────────┘  └──────────────┘  └────┘                 
pid           └┘        └─────────────┘└─────┘           └─────┘                        
st   ───┘└─────┘└──────────────────────────────────────────────┘└──────────────────────────┘└┘
518    unfold padic_seq.norm at hge; split_ifs at hge,
src    └──────────────────────────┘  └──────────────┘
typ    └──────────────────────────┘  └──────────────┘
doc    └──────────────────────────┘  └──────────────┘
txt    └──────────────────────────┘  └──────────────┘
par    └──────────────────────────┘  └──────────────┘
pid          └─────────────┘└─────┘           └─────┘
st   ───────────────────────────────────────────────┘└─
519    apply not_le_of_gt _ hge,
id           └──────────┘   └─┘
src    └────┘└──────────┘└─┘
typ    └────┘└──────────┘└─┘└─┘
doc    └────┘            └─┘
txt    └────┘            └─┘
par    └────┘            └─┘
pid                     └─┘
st   ─────────────────────────┘└─
520    cases decidable.em ((stationary_point hne) ≥ N) with hgen hngen,
id           └──────────┘   └──────────────┘ └─┘    
src    └────┘└──────────┘  └──────────────┘   └┘  └───────────────┘
typ    └────┘└──────────┘  └──────────────┘└─┘└┘ └───────────────┘
doc    └────┘              └──────────────┘   └┘  └───────────────┘
txt    └────┘                                 └┘  └───────────────┘
par    └────┘                                 └┘  └───────────────┘
pid                                          └┘  └──────────────┘
st   ────────────────────────────────────────────────────────────────┘└─
521    { apply hN; assumption },
src      └────┘    └─────────┘
typ      └────┘    └─────────┘
doc      └────┘    └─────────┘
txt      └────┘    └─────────┘
par      └────┘    └─────────┘
pid                         
st   ───┘└───────────────────┘└┘
522    { have := stationary_point_spec hne (le_refl _) (le_of_not_le hngen),
id               └───────────────────┘ └─┘  └─────┘     └──────────┘ └───┘
src      └──────┘└───────────────────┘    └─────┘└──┘ └──────────┘     
typ      └──────┘└───────────────────┘└─┘ └─────┘└──┘ └──────────┘└───┘
doc      └──────┘                                └──┘                  
txt      └──────┘                                └──┘                  
par      └──────┘                                └──┘                  
pid      └───┘└─┘                                └──┘                  
st   ─────────────────────────────────────────────────────────────────────┘└─
523      rw ←this,
id           └──┘
src      └──┘
typ      └──┘└──┘
doc      └──┘
txt      └──┘
par      └──┘
pid        └┘
st   ───────────┘└─
524      apply hN,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
525      apply le_refl, assumption }
id             └─────┘
src      └────┘└─────┘  └─────────┘
typ      └────┘└─────┘  └─────────┘
doc      └────┘         └─────────┘
txt      └────┘         └─────────┘
par      └────┘         └─────────┘
pid                              
st   ────────────────┘└───────────┘└─
526  end
st   ──┘
527  
528  protected lemma nonneg (q : ℚ_[p]) : padic_norm_e q ≥ 0 :=
id                               └─┘    └──────────┘  
src                              └─┘     └──────────┘   
typ                              └─┘    └──────────┘  
doc                              └─┘     └──────────┘
529  quotient.induction_on q $ norm_nonneg
id   └───────────────────┘    └─────────┘
src  └───────────────────┘     └─────────┘
typ  └───────────────────┘    └─────────┘
530  
531  lemma zero_def : (0 : ℚ_[p]) = ⟦0⟧ := rfl
id                         └─┘        └─┘
src                        └─┘         └─┘
typ                        └─┘        └─┘
doc                        └─┘ 
532  
533  lemma zero_iff (q : ℚ_[p]) : padic_norm_e q = 0 ↔ q = 0 :=
id                       └─┘    └──────────┘       
src                      └─┘     └──────────┘         
typ                      └─┘    └──────────┘       
doc                      └─┘     └──────────┘
534  quotient.induction_on q $
id   └───────────────────┘ 
src  └───────────────────┘
typ  └───────────────────┘ 
535    by simpa only [zero_def, quotient.eq] using norm_zero_iff
id                    └──────┘  └─────────┘        └───────────┘
src       └──────────┘└──────┘└┘└─────────┘└──────┘└───────────┘
typ       └──────────┘└──────┘└┘└─────────┘└──────┘└───────────┘
doc       └──────────┘        └┘           └──────┘             
txt       └──────────┘        └┘           └──────┘             
par       └──────────┘        └┘           └──────┘             
pid            └──┘└┘        └┘           └────┘             
st       └───────────────────────────────────────────────────────
536  
src  
typ  
doc  
txt  
par  
pid  
st   
537  @[simp] protected lemma zero : padic_norm_e (0 : ℚ_[p]) = 0 :=
id                                  └──────────┘      └─┘  
src                                 └──────────┘      └─┘   
typ                                 └──────────┘      └─┘  
doc    └──┘                         └──────────┘      └─┘ 
538  (zero_iff _).2 rfl
id    └──────┘     └─┘
src   └──────┘     └─┘
typ   └──────┘     └─┘
539  
540  /-- Theorems about `padic_norm_e` are named with a `'` so the names do not conflict with the
541  equivalent theorems about `norm` (`∥ ∥`). -/
542  @[simp] protected lemma one' : padic_norm_e (1 : ℚ_[p]) = 1 :=
id                                  └──────────┘      └─┘  
src                                 └──────────┘      └─┘   
typ                                 └──────────┘      └─┘  
doc    └──┘                         └──────────┘      └─┘ 
543  norm_one
id   └──────┘
src  └──────┘
typ  └──────┘
544  
545  @[simp] protected lemma neg (q : ℚ_[p]) : padic_norm_e (-q) = padic_norm_e q :=
id                                    └─┘    └──────────┘     └──────────┘ 
src                                   └─┘     └──────────┘      └──────────┘
typ                                   └─┘    └──────────┘     └──────────┘ 
doc    └──┘                           └─┘     └──────────┘        └──────────┘
546  quotient.induction_on q $ norm_neg
id   └───────────────────┘    └──────┘
src  └───────────────────┘     └──────┘
typ  └───────────────────┘    └──────┘
547  
548  /-- Theorems about `padic_norm_e` are named with a `'` so the names do not conflict with the
549  equivalent theorems about `norm` (`∥ ∥`). -/
550  theorem nonarchimedean' (q r : ℚ_[p]) :
id                                  └─┘
src                                 └─┘ 
typ                                 └─┘
doc                                 └─┘ 
551    padic_norm_e (q + r) ≤ max (padic_norm_e q) (padic_norm_e r) :=
id     └──────────┘       └─┘  └──────────┘    └──────────┘ 
src    └──────────┘         └─┘  └──────────┘     └──────────┘
typ    └──────────┘       └─┘  └──────────┘    └──────────┘ 
doc    └──────────┘                └──────────┘     └──────────┘
552  quotient.induction_on₂ q r $ norm_nonarchimedean
id   └────────────────────┘     └─────────────────┘
src  └────────────────────┘       └─────────────────┘
typ  └────────────────────┘     └─────────────────┘
553  
554  /-- Theorems about `padic_norm_e` are named with a `'` so the names do not conflict with the
555  equivalent theorems about `norm` (`∥ ∥`). -/
556  theorem add_eq_max_of_ne' {q r : ℚ_[p]} :
id                                    └─┘
src                                   └─┘ 
typ                                   └─┘
doc                                   └─┘ 
557    padic_norm_e q ≠ padic_norm_e r → padic_norm_e (q + r) = max (padic_norm_e q) (padic_norm_e r) :=
id     └──────────┘   └──────────┘    └──────────┘       └─┘  └──────────┘    └──────────┘ 
src    └──────────┘    └──────────┘     └──────────┘         └─┘  └──────────┘     └──────────┘
typ    └──────────┘   └──────────┘    └──────────┘       └─┘  └──────────┘    └──────────┘ 
doc    └──────────┘     └──────────┘     └──────────┘                └──────────┘     └──────────┘
558  quotient.induction_on₂ q r $ λ _ _, padic_seq.add_eq_max_of_ne
id   └────────────────────┘          └────────────────────────┘
src  └────────────────────┘              └────────────────────────┘
typ  └────────────────────┘          └────────────────────────┘
559  
560  lemma triangle_ineq (x y z : ℚ_[p]) :
id                                └─┘
src                               └─┘ 
typ                               └─┘
doc                               └─┘ 
561    padic_norm_e (x - z) ≤ padic_norm_e (x - y) + padic_norm_e (y - z) :=
id     └──────────┘       └──────────┘       └──────────┘    
src    └──────────┘         └──────────┘         └──────────┘    
typ    └──────────┘       └──────────┘       └──────────┘    
doc    └──────────┘           └──────────┘           └──────────┘
562  calc padic_norm_e (x - z) = padic_norm_e ((x - y) + (y - z)) : by rw sub_add_sub_cancel
id        └──────────┘        └──────────┘                      └────────────────┘
src       └──────────┘          └──────────┘                       └─┘└────────────────┘
typ       └──────────┘        └──────────┘                   └─┘└────────────────┘
doc       └──────────┘           └──────────┘                          └─┘                  
txt                                                                    └─┘                  
par                                                                    └─┘                  
pid                                                                                        
st                                                                    └──────────────────────
563    ... ≤ max (padic_norm_e (x - y)) (padic_norm_e (y - z)) : padic_norm_e.nonarchimedean' _ _
id           └─┘  └──────────┘        └──────────┘         └──────────────────────────┘
src  ─┘      └─┘  └──────────┘          └──────────┘           └──────────────────────────┘
typ  ─┘      └─┘  └──────────┘        └──────────┘         └──────────────────────────┘
doc  ─┘           └──────────┘           └──────────┘            └──────────────────────────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
564    ... ≤ padic_norm_e (x - y) + padic_norm_e (y - z) :
id           └──────────┘       └──────────┘    
src          └──────────┘         └──────────┘    
typ          └──────────┘       └──────────┘    
doc          └──────────┘           └──────────┘
565      max_le_add_of_nonneg (padic_norm_e.nonneg _) (padic_norm_e.nonneg _)
id       └──────────────────┘  └─────────────────┘     └─────────────────┘
src      └──────────────────┘  └─────────────────┘     └─────────────────┘
typ      └──────────────────┘  └─────────────────┘     └─────────────────┘
566  
567  protected lemma add (q r : ℚ_[p]) : padic_norm_e (q + r) ≤ (padic_norm_e q) + (padic_norm_e r) :=
id                              └─┘    └──────────┘        └──────────┘     └──────────┘ 
src                             └─┘     └──────────┘          └──────────┘      └──────────┘
typ                             └─┘    └──────────┘        └──────────┘     └──────────┘ 
doc                             └─┘     └──────────┘            └──────────┘       └──────────┘
568  calc
569    padic_norm_e (q + r) ≤ max (padic_norm_e q) (padic_norm_e r) : nonarchimedean' _ _
id     └──────────┘        └─┘  └──────────┘    └──────────┘     └─────────────┘
src    └──────────┘          └─┘  └──────────┘     └──────────┘      └─────────────┘
typ    └──────────┘        └─┘  └──────────┘    └──────────┘     └─────────────┘
doc    └──────────┘                └──────────┘     └──────────┘      └─────────────┘
570                        ... ≤ (padic_norm_e q) + (padic_norm_e r) :
id                                └──────────┘     └──────────┘ 
src                               └──────────┘      └──────────┘
typ                               └──────────┘     └──────────┘ 
doc                               └──────────┘       └──────────┘
571                                max_le_add_of_nonneg (padic_norm_e.nonneg _) (padic_norm_e.nonneg _)
id                                 └──────────────────┘  └─────────────────┘     └─────────────────┘
src                                └──────────────────┘  └─────────────────┘     └─────────────────┘
typ                                └──────────────────┘  └─────────────────┘     └─────────────────┘
572  
573  protected lemma mul' (q r : ℚ_[p]) : padic_norm_e (q * r) = (padic_norm_e q) * (padic_norm_e r) :=
id                               └─┘    └──────────┘        └──────────┘     └──────────┘ 
src                              └─┘     └──────────┘          └──────────┘      └──────────┘
typ                              └─┘    └──────────┘        └──────────┘     └──────────┘ 
doc                              └─┘     └──────────┘            └──────────┘       └──────────┘
574  quotient.induction_on₂ q r $ norm_mul
id   └────────────────────┘     └──────┘
src  └────────────────────┘       └──────┘
typ  └────────────────────┘     └──────┘
575  
576  instance : is_absolute_value (@padic_norm_e p _) :=
id              └───────────────┘   └──────────┘ 
src             └───────────────┘   └──────────┘
typ             └───────────────┘   └──────────┘ 
doc             └───────────────┘   └──────────┘
577  { abv_nonneg := padic_norm_e.nonneg,
id                   └─────────────────┘
src                  └─────────────────┘
typ                  └─────────────────┘
578    abv_eq_zero := zero_iff,
id                    └──────┘
src                   └──────┘
typ                   └──────┘
579    abv_add := padic_norm_e.add,
id                └──────────────┘
src               └──────────────┘
typ               └──────────────┘
580    abv_mul := padic_norm_e.mul' }
id                └───────────────┘
src               └───────────────┘
typ               └───────────────┘
581  
582  @[simp] lemma eq_padic_norm' (q : ℚ) : padic_norm_e (padic.of_rat p q) = padic_norm p q :=
id                                         └──────────┘  └──────────┘     └────────┘  
src                                        └──────────┘  └──────────┘       └────────┘
typ                                        └──────────┘  └──────────┘     └────────┘  
doc    └──┘                                └──────────┘  └──────────┘        └────────┘
583  norm_const _
id   └────────┘
src  └────────┘
typ  └────────┘
584  
585  protected theorem image' {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, padic_norm_e q = p ^ (-n) :=
id                                 └─┘                └──────────┘      
src                                └─┘                  └──────────┘        
typ                                └─┘                └──────────┘      
doc                                └─┘                      └──────────┘
586  quotient.induction_on q $ λ f hf,
id   └───────────────────┘       └┘
src  └───────────────────┘
typ  └───────────────────┘       └┘
587    have ¬ f ≈ 0, from (ne_zero_iff_nequiv_zero f).1 hf,
id                      └─────────────────────┘    └┘
src                      └─────────────────────┘   
typ                     └─────────────────────┘    └┘
588    norm_image f this
id     └────────┘  └──┘
src    └────────┘
typ    └────────┘  └──┘
589  
590  lemma sub_rev (q r : ℚ_[p]) : padic_norm_e (q - r) = padic_norm_e (r - q) :=
id                        └─┘    └──────────┘       └──────────┘    
src                       └─┘     └──────────┘         └──────────┘    
typ                       └─┘    └──────────┘       └──────────┘    
doc                       └─┘     └──────────┘           └──────────┘
591  by rw ←(padic_norm_e.neg); simp
id           └──────────────┘
src     └──┘ └──────────────┘  └────
typ     └──┘ └──────────────┘  └────
doc     └──┘                   └────
txt     └──┘                   └────
par     └──┘                   └────
pid       └┘                       
st     └─────────────────────────────
592  
src  
typ  
doc  
txt  
par  
pid  
st   
593  end embedding
594  end padic_norm_e
595  
596  namespace padic
597  
598  section complete
599  open padic_seq padic
600  
601  theorem rat_dense' {p : ℕ} [nat.prime p] (q : ℚ_[p]) {ε : ℚ} (hε : ε > 0) :
id                              └───────┘        └─┘                
src                             └───────┘         └─┘                  
typ                             └───────┘        └─┘                
doc                              └───────┘         └─┘        
602    ∃ r : ℚ, padic_norm_e (q - r) < ε :=
id           └──────────┘       
src          └──────────┘        
typ          └──────────┘       
doc            └──────────┘
603  quotient.induction_on q $ λ q',
id   └───────────────────┘      └┘
src  └───────────────────┘
typ  └───────────────────┘      └┘
604    have ∃ N, ∀ m n ≥ N, padic_norm p (q' m - q' n) < ε, from cauchy₂ _ hε,
id                    └────────┘   └┘   └┘           └─────┘   └┘
src                       └────────┘                         └─────┘
typ                   └────────┘   └┘   └┘           └─────┘   └┘
doc                         └────────┘
605    let ⟨N, hN⟩ := this in
id     └─┘           └──┘
typ    └─┘           └──┘
606    ⟨q' N,
id      └┘
typ     └┘
607      begin
st       └─────
608        simp only [padic.cast_eq_of_rat],
id                    └──────────────────┘
src        └─────────┘└──────────────────┘
typ        └─────────┘└──────────────────┘
doc        └─────────┘                    
txt        └─────────┘                    
par        └─────────┘                    
pid            └──┘└┘                    
st   ─────────────────────────────────────┘└─
609        change padic_seq.norm (q' - const _ (q' N)) < ε,
id                └────────────┘      └───┘    └┘     
src        └─────┘└────────────┘   └───┘└─┘    └─┘
typ        └─────┘└────────────┘   └───┘└─┘ └┘└─┘
doc        └─────┘└────────────┘    └───┘└─┘    └─┘ 
txt        └─────┘                       └─┘    └─┘ 
par        └─────┘                       └─┘    └─┘ 
pid                                     └─┘    └─┘ 
st   ────────────────────────────────────────────────────┘└─
610        cases decidable.em ((q' - const (padic_norm p) (q' N)) ≈ 0) with heq hne',
id               └──────────┘        └───┘  └────────┘    └┘    
src        └────┘└──────────┘     └───┘ └────────┘ └┘    └─┘└───────────────┘
typ        └────┘└──────────┘     └───┘ └────────┘└┘ └┘└─┘└───────────────┘
doc        └────┘                 └───┘ └────────┘ └┘    └─┘ └───────────────┘
txt        └────┘                                  └┘    └─┘ └───────────────┘
par        └────┘                                  └┘    └─┘ └───────────────┘
pid                                               └┘    └─┘ └─┘└────────────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
611        { simpa only [heq, padic_seq.norm, dif_pos] },
id                       └─┘  └────────────┘  └─────┘
src          └──────────┘└─┘└┘└────────────┘└┘└─────┘└┘
typ          └──────────┘└─┘└┘└────────────┘└┘└─────┘└┘
doc          └──────────┘   └┘└────────────┘└┘       └┘
txt          └──────────┘   └┘              └┘       └┘
par          └──────────┘   └┘              └┘       └┘
pid               └──┘└┘   └┘              └┘       
st   ───────┘└────────────────────────────────────────┘└┘
612        { simp only [padic_seq.norm, dif_neg hne'],
id                      └────────────┘  └─────┘ └──┘
src          └─────────┘└────────────┘└┘└─────┘    
typ          └─────────┘└────────────┘└┘└─────┘└──┘
doc          └─────────┘└────────────┘└┘           
txt          └─────────┘              └┘           
par          └─────────┘              └┘           
pid              └──┘└┘              └┘           
st   ───────────────────────────────────────────────┘└─
613          change padic_norm p (q' _ - q' _) < ε,
id                  └────────┘          └┘      
src          └─────┘└────────┘    └─┘   └──┘ 
typ          └─────┘└────────┘   └─┘ └┘└──┘ 
doc          └─────┘└────────┘    └─┘   └──┘ 
txt          └─────┘              └─┘   └──┘ 
par          └─────┘              └─┘   └──┘ 
pid                              └─┘   └──┘ 
st   ────────────────────────────────────────────┘└─
614          have := stationary_point_spec hne',
id                   └───────────────────┘ └──┘
src          └──────┘└───────────────────┘
typ          └──────┘└───────────────────┘└──┘
doc          └──────┘                     
txt          └──────┘                     
par          └──────┘                     
pid          └───┘└─┘                     
st   ─────────────────────────────────────────┘└─
615          cases decidable.em (N ≥ stationary_point hne') with hle hle,
id                 └──────────┘    └──────────────┘ └──┘
src          └────┘└──────────┘  └──────────────┘    └────────────┘
typ          └────┘└──────────┘ └──────────────┘└──┘└────────────┘
doc          └────┘               └──────────────┘    └────────────┘
txt          └────┘                                   └────────────┘
par          └────┘                                   └────────────┘
pid                                                  └───────────┘
st   ──────────────────────────────────────────────────────────────────┘└─
616          { have := eq.symm (this (le_refl _) hle),
id                     └─────┘  └──┘  └─────┘    └─┘
src            └──────┘└─────┘      └─────┘└──┘   
typ            └──────┘└─────┘ └──┘ └─────┘└──┘└─┘
doc            └──────┘                    └──┘   
txt            └──────┘                    └──┘   
par            └──────┘                    └──┘   
pid            └───┘└─┘                    └──┘   
st   ─────────┘└────────────────────────────────────┘└─
617            simp at this, simpa [this] },
id                                  └──┘
src            └──────────┘  └─────┘    └┘
typ            └──────────┘  └─────┘└──┘└┘
doc            └──────────┘  └─────┘    └┘
txt            └──────────┘  └─────┘    └┘
par            └──────────┘  └─────┘    └┘
pid                └─────┘           
st   ─────────────────────┘└─────────────┘└┘
618          { apply hN,
src            └────┘
typ            └────┘
doc            └────┘
txt            └────┘
par            └────┘
pid                 
st   ─────────────────┘└─
619            apply le_of_lt, apply lt_of_not_ge, apply hle, apply le_refl }}
id                   └──────┘        └──────────┘                   └─────┘
src            └────┘└──────┘  └────┘└──────────┘  └────┘     └────┘└─────┘
typ            └────┘└──────┘  └────┘└──────────┘  └────┘     └────┘└─────┘
doc            └────┘          └────┘              └────┘     └────┘       
txt            └────┘          └────┘              └────┘     └────┘       
par            └────┘          └────┘              └────┘     └────┘       
pid                                                                    
st   ───────────────────────┘└──────────────────┘└─────────┘└──────────────┘└──
620      end⟩
st   ──────┘
621  
622  variables {p : ℕ} [nat.prime p] (f : cau_seq _ (@padic_norm_e p _))
id                     └───────┘         └─────┘     └──────────┘
src                    └───────┘         └─────┘     └──────────┘
typ                    └───────┘         └─────┘     └──────────┘
doc                     └───────┘                     └──────────┘
623  open classical
624  
625  private lemma div_nat_pos (n : ℕ) : (1 / ((n + 1): ℚ)) > 0 :=
id                                                     
src                                                     
typ                                                    
doc                                                     
626  div_pos zero_lt_one (by exact_mod_cast succ_pos _)
id   └─────┘ └─────────┘                    └──────┘
src  └─────┘ └─────────┘     └─────────────┘└──────┘└┘
typ  └─────┘ └─────────┘     └─────────────┘└──────┘└┘
doc                          └─────────────┘        └┘
txt                          └─────────────┘        └┘
par                          └─────────────┘        └┘
pid                                                └┘
st                          └────────────────────────┘
627  
628  def lim_seq : ℕ → ℚ := λ n, classical.some (rat_dense' (f n) (div_nat_pos n))
id                            └────────────┘  └────────┘      └─────────┘ 
src                            └────────────┘  └────────┘        └─────────┘
typ                           └────────────┘  └────────┘      └─────────┘ 
doc                    
629  
630  lemma exi_rat_seq_conv {ε : ℚ} (hε : 0 < ε) :
id                                          
src                                        
typ                                         
doc                              
631    ∃ N, ∀ i ≥ N, padic_norm_e (f i - ((lim_seq f) i : ℚ_[p])) < ε :=
id              └──────────┘       └─────┘      └─┘    
src                └──────────┘         └─────┘        └─┘    
typ             └──────────┘       └─────┘      └─┘    
doc                  └──────────┘                         └─┘ 
632  begin
st   └─────
633    refine (exists_nat_gt (1/ε)).imp (λ N hN i hi, _),
id             └───────────┘   
src    └─────┘ └───────────┘  └─────┘  └────────────┘
typ    └─────┘ └───────────┘ └─────┘  └────────────┘
doc    └─────┘                 └─────┘  └────────────┘
txt    └─────┘                 └─────┘  └────────────┘
par    └─────┘                 └─────┘  └────────────┘
pid                           └─────┘  └────────────┘
st   ──────────────────────────────────────────────────┘└─
634    have h := classical.some_spec (rat_dense' (f i) (div_nat_pos i)),
id               └─────────────────┘  └────────┘       └─────────┘ 
src    └────────┘└─────────────────┘ └────────┘   └┘ └─────────┘ └┘
typ    └────────┘└─────────────────┘ └────────┘  └┘ └─────────┘└┘
doc    └────────┘                                 └┘             └┘
txt    └────────┘                                 └┘             └┘
par    └────────┘                                 └┘             └┘
pid    └────┘└─┘                                 └┘             └┘
st   ─────────────────────────────────────────────────────────────────┘└─
635    refine lt_of_lt_of_le h (div_le_of_le_mul (by exact_mod_cast succ_pos _) _),
id            └────────────┘   └──────────────┘                    └──────┘
src    └─────┘└────────────┘  └──────────────┘   └─────────────┘└──────┘└┘└──┘
typ    └─────┘└────────────┘ └──────────────┘   └──────────────┘└──────┘└────┘
doc    └─────┘                                   └─────────────┘        └┘└──┘
txt    └─────┘                                   └─────────────┘        └┘└──┘
par    └─────┘                                   └──────────────┘        └────┘
pid                                             └──────────────┘        └────┘
st   ──────────────────────────────────────────────┘└────────────────────────┘└──┘└─
636    rw right_distrib,
id        └───────────┘
src    └─┘└───────────┘
typ    └─┘└───────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────┘└─
637    apply le_add_of_le_of_nonneg,
id           └────────────────────┘
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────────┘└─
638    { exact le_mul_of_div_le hε (le_trans (le_of_lt hN) (by exact_mod_cast hi)) },
id             └──────────────┘ └┘  └──────┘  └──────┘ └┘                     └┘
src      └────┘└──────────────┘   └──────┘ └──────┘  └┘   └─────────────┘  └─┘
typ      └────┘└──────────────┘└┘ └──────┘ └──────┘└┘└┘   └──────────────┘└┘└─┘
doc      └────┘                                      └┘   └─────────────┘  └─┘
txt      └────┘                                      └┘   └─────────────┘  └─┘
par      └────┘                                      └┘   └──────────────┘  └─┘
pid                                                 └┘   └──────────────┘  └┘
st   ───┘└───────────────────────────────────────────────────┘└────────────────┘└─┘└┘
639    { apply le_of_lt, simpa }
id             └──────┘
src      └────┘└──────┘  └────┘
typ      └────┘└──────┘  └────┘
doc      └────┘          └────┘
txt      └────┘          └────┘
par      └────┘          └────┘
pid                          
st   ─────────────────┘└──────┘└─
640  end
st   ──┘
641  
642  lemma exi_rat_seq_conv_cauchy : is_cau_seq (padic_norm p) (lim_seq f) :=
id                                   └────────┘  └────────┘    └─────┘ 
src                                  └────────┘  └────────┘     └─────┘
typ                                  └────────┘  └────────┘    └─────┘ 
doc                                  └────────┘  └────────┘
643  assume ε hε,
id           └┘
typ          └┘
644  have hε3 : ε / 3 > 0, from div_pos hε (by norm_num),
id                           └─────┘ └┘
src                           └─────┘        └──────┘
typ                          └─────┘ └┘     └──────┘
doc                                            └──────┘
txt                                            └──────┘
par                                            └──────┘
st                                            └───────┘
645  let ⟨N, hN⟩ := exi_rat_seq_conv f hε3,
id   └─┘            └──────────────┘  └─┘
src                 └──────────────┘
typ  └─┘            └──────────────┘  └─┘
646      ⟨N2, hN2⟩ := f.cauchy₂ hε3 in
id                    └──────┘ └─┘
src                    └──────┘
typ                   └──────┘ └─┘
647  begin
st   └─────
648    existsi max N N2,
id             └─┘  └┘
src    └──────┘└─┘ 
typ    └──────┘└─┘└┘
doc    └──────┘    
txt    └──────┘    
par    └──────┘    
pid               
st   ─────────────────┘└─
649    intros j hj,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
650    suffices : padic_norm_e ((↑(lim_seq f j) - f (max N N2)) + (f (max N N2) - lim_seq f (max N N2))) < ε,
id                └──────────┘                                                └─────┘   └─┘  └┘     
src    └─────────┘└──────────┘            └┘        └─┘         └┘ └─────┘  └─┘   └──┘
typ    └─────────┘└──────────┘           └┘        └─┘         └┘ └─────┘ └─┘└┘└──┘
doc    └─────────┘└──────────┘             └┘         └─┘          └┘                └──┘ 
txt    └─────────┘                         └┘         └─┘          └┘                └──┘ 
par    └─────────┘                         └┘         └─┘          └┘                └──┘ 
pid    └───────┘└┘                         └┘         └─┘          └┘                └──┘ 
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
651    { ring at this ⊢,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid          └───────┘
st   ───┘└────────────┘└─
652      rw [← padic_norm_e.eq_padic_norm', ← padic.cast_eq_of_rat],
id             └─────────────────────────┘    └──────────────────┘
src      └────┘└─────────────────────────┘└──┘└──────────────────┘
typ      └────┘└─────────────────────────┘└──┘└──────────────────┘
doc      └────┘                           └──┘                    
txt      └────┘                           └──┘                    
par      └────┘                           └──┘                    
pid        └──┘                           └──┘                    
st   ────────────────────────────────────┘└──────────────────────┘└──
653      exact_mod_cast this },
id                      └──┘
src      └─────────────┘    
typ      └─────────────┘└──┘
doc      └─────────────┘    
txt      └─────────────┘    
par      └─────────────┘    
pid                        
st   ───────────────────────┘└┘
654    { apply lt_of_le_of_lt,
id             └────────────┘
src      └────┘└────────────┘
typ      └────┘└────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────┘└─
655      { apply padic_norm_e.add },
id               └──────────────┘
src        └────┘└──────────────┘
typ        └────┘└──────────────┘
doc        └────┘                
txt        └────┘                
par        └────┘                
pid                             
st   ─────┘└─────────────────────┘└┘
656      { have : (3 : ℚ) ≠ 0, by norm_num,
id                        
src        └─────┘ └──┘ └┘└┘     └──────┘
typ        └─────┘ └──┘ └┘└┘     └──────┘
doc        └─────┘ └──┘ └┘ └┘     └──────┘
txt        └─────┘ └──┘ └┘ └┘     └──────┘
par        └─────┘ └──┘ └┘ └┘     └──────┘
pid        └───┘└┘ └──┘ └┘ 
st   ───────────────────────┘             └─
657        have : ε = ε / 3 + ε / 3 + ε / 3,
id                                  
src        └─────┘  └─┘   └─┘   └┘
typ        └─────┘  └─┘   └─┘  └┘
doc        └─────┘    └─┘   └─┘   └┘
txt        └─────┘    └─┘   └─┘   └┘
par        └─────┘    └─┘   └─┘   └┘
pid        └───┘└┘    └─┘   └─┘   
st   ─────────────────────────────────────┘└─
658        { apply eq_of_mul_eq_mul_left this, simp [left_distrib, mul_div_cancel' _ this ], ring },
id                 └───────────────────┘ └──┘        └──────────┘  └─────────────┘   └──┘
src          └────┘└───────────────────┘      └────┘└──────────┘└┘└─────────────┘└─┘    └┘  └───┘
typ          └────┘└───────────────────┘└──┘  └────┘└──────────┘└┘└─────────────┘└─┘└──┘└┘  └───┘
doc          └────┘                           └────┘            └┘               └─┘    └┘  └───┘
txt          └────┘                           └────┘            └┘               └─┘    └┘  └───┘
par          └────┘                           └────┘            └┘               └─┘    └┘  └───┘
pid                                                          └┘               └─┘    └┘      
st   ───────┘└──────────────────────────────┘└────────────────────────────────────────────┘└─────┘└┘
659        rw this,
id            └──┘
src        └─┘
typ        └─┘└──┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────┘└─
660        apply add_lt_add,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
661        { suffices : padic_norm_e ((↑(lim_seq f j) - f j) + (f j - f (max N N2))) < ε / 3 + ε / 3,
id                      └──────────┘     └─────┘                       └─┘  └┘              
src          └─────────┘└──────────┘    └─────┘  └┘   └┘       └─┘   └──┘   └─┘   └┘
typ          └─────────┘└──────────┘    └─────┘  └┘   └┘     └─┘└┘└──┘   └─┘  └┘
doc          └─────────┘└──────────┘             └┘   └┘             └──┘   └─┘   └┘
txt          └─────────┘                         └┘   └┘             └──┘   └─┘   └┘
par          └─────────┘                         └┘   └┘             └──┘   └─┘   └┘
pid          └───────┘└┘                         └┘   └┘             └──┘   └─┘   
st   ───────┘└─────────────────────────────────────────────────────────────────────────────────────┘
662            by simpa,
src               └───┘
typ               └───┘
doc               └───┘
txt               └───┘
par               └───┘
st                     └─
663          apply lt_of_le_of_lt,
id                 └────────────┘
src          └────┘└────────────┘
typ          └────┘└────────────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────────────────────────┘└─
664          { apply padic_norm_e.add },
id                   └──────────────┘
src            └────┘└──────────────┘
typ            └────┘└──────────────┘
doc            └────┘                
txt            └────┘                
par            └────┘                
pid                                 
st   ─────────┘└─────────────────────┘└┘
665          { apply add_lt_add,
id                   └────────┘
src            └────┘└────────┘
typ            └────┘└────────┘
doc            └────┘
txt            └────┘
par            └────┘
pid                 
st   ─────────────────────────┘└─
666            { rw [padic_norm_e.sub_rev],
id                   └──────────────────┘
src              └──┘└──────────────────┘
typ              └──┘└──────────────────┘
doc              └──┘                    
txt              └──┘                    
par              └──┘                    
pid                └┘                    
st   ───────────┘└──────────────────────┘└──
667              apply_mod_cast hN,
src              └─────────────┘
typ              └─────────────┘
doc              └─────────────┘
txt              └─────────────┘
par              └─────────────┘
pid                            
st   ────────────────────────────┘└─
668              exact le_of_max_le_left hj },
id                     └───────────────┘ └┘
src              └────┘└───────────────┘  
typ              └────┘└───────────────┘└┘
doc              └────┘                   
txt              └────┘                   
par              └────┘                   
pid                                      
st   ──────────────────────────────────────┘└┘
669            { apply hN2,
src              └────┘
typ              └────┘
doc              └────┘
txt              └────┘
par              └────┘
pid                   
st   ────────────────────┘└─
670              exact le_of_max_le_right hj,
id                     └────────────────┘ └┘
src              └────┘└────────────────┘
typ              └────┘└────────────────┘└┘
doc              └────┘                  
txt              └────┘                  
par              └────┘                  
pid                                     
st   ──────────────────────────────────────┘└─
671              apply le_max_right }}},
id                     └──────────┘
src              └────┘└──────────┘
typ              └────┘└──────────┘
doc              └────┘            
txt              └────┘            
par              └────┘            
pid                               
st   ──────────────────────────────┘└──┘
672        { apply_mod_cast hN,
src          └─────────────┘
typ          └─────────────┘
doc          └─────────────┘
txt          └─────────────┘
par          └─────────────┘
pid                        
st   ────────────────────────┘└─
673          apply le_max_left }}}
id                 └─────────┘
src          └────┘└─────────┘
typ          └────┘└─────────┘
doc          └────┘           
txt          └────┘           
par          └────┘           
pid                          
st   ─────────────────────────┘└───
674  end
st   ──┘
675  
676  private def lim' : padic_seq p := ⟨_, exi_rat_seq_conv_cauchy f⟩
id                      └───────┘         └─────────────────────┘ 
src                     └───────┘          └─────────────────────┘
typ                     └───────┘         └─────────────────────┘ 
doc                     └───────┘
677  
678  private def lim : ℚ_[p] := ⟦lim' f⟧
id                     └─┘    └──┘ 
src                    └─┘     └──┘  
typ                    └─┘    └──┘ 
doc                    └─┘ 
679  
680  theorem complete' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padic_norm_e (q - f i) < ε :=
id                            └─┘                  └──────────┘        
src                           └─┘                      └──────────┘          
typ                           └─┘                  └──────────┘        
doc                            └─┘                          └──────────┘
681  ⟨ lim f,
id     └─┘ 
src    └─┘
typ    └─┘ 
682    λ ε hε,
id        └┘
typ       └┘
683    let ⟨N, hN⟩ := exi_rat_seq_conv f (show ε / 2 > 0, from div_pos hε (by norm_num)),
id     └─┘            └──────────────┘                     └─────┘ └┘
src                   └──────────────┘                       └─────┘        └──────┘
typ    └─┘            └──────────────┘                     └─────┘ └┘     └──────┘
doc                                                                           └──────┘
txt                                                                           └──────┘
par                                                                           └──────┘
st                                                                           └───────┘
684        ⟨N2, hN2⟩ := padic_norm_e.defn (lim' f) (show ε / 2 > 0, from div_pos hε (by norm_num)) in
id                      └───────────────┘  └──┘                      └─────┘ └┘
src                     └───────────────┘  └──┘                        └─────┘        └──────┘
typ                     └───────────────┘  └──┘                      └─────┘ └┘     └──────┘
doc                                                                                     └──────┘
txt                                                                                     └──────┘
par                                                                                     └──────┘
st                                                                                     └───────┘
685    begin
st     └─────
686      existsi max N N2,
id               └─┘  └┘
src      └──────┘└─┘ 
typ      └──────┘└─┘└┘
doc      └──────┘    
txt      └──────┘    
par      └──────┘    
pid                 
st   ───────────────────┘└─
687      intros i hi,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
688      suffices : padic_norm_e ((lim f - lim' f i) + (lim' f i - f i)) < ε,
id                  └──────────┘   └─┘                └──┘            
src      └─────────┘└──────────┘  └─┘       └┘ └──┘     └─┘
typ      └─────────┘└──────────┘  └─┘       └┘ └──┘   └─┘
doc      └─────────┘└──────────┘             └┘           └─┘ 
txt      └─────────┘                         └┘           └─┘ 
par      └─────────┘                         └┘           └─┘ 
pid      └───────┘└┘                         └┘           └─┘ 
st   ──────────────────────────────────────────────────────────────────────┘└─
689      { ring at this; exact this },
id                             └──┘
src        └──────────┘  └────┘    
typ        └──────────┘  └────┘└──┘
doc        └──────────┘  └────┘    
txt        └──────────┘  └────┘    
par        └──────────┘  └────┘    
pid            └─────┘           
st   ─────┘└───────────────────────┘
690      { apply lt_of_le_of_lt,
691        { apply padic_norm_e.add },
st                                  
692        { have : ε = ε / 2 + ε / 2, by rw ←(add_self_div_two ε); simp,
id                                            └──────────────┘ 
src                                       └──┘ └──────────────┘   └──┘
typ                                      └──┘ └──────────────┘  └──┘
doc                                       └──┘                    └──┘
txt                                       └──┘                    └──┘
par                                       └──┘                    └──┘
pid                                         └┘                  
693          rw this,
694          apply add_lt_add,
695          { apply hN2, exact le_of_max_le_right hi },
st                                                    
696          { rw_mod_cast [padic_norm_e.sub_rev],
src                                             
typ                                             
doc                                             
txt                                             
par                                             
pid                                             
697            apply hN,
698            exact le_of_max_le_left hi }}}
st                                        └───
699    end ⟩
st   ────┘
700  
701  end complete
702  
703  section normed_space
704  variables (p : ℕ) [nat.prime p]
id                     └───────┘
src                    └───────┘
typ                    └───────┘
doc                     └───────┘
705  
706  instance : has_dist ℚ_[p] := ⟨λ x y, padic_norm_e (x - y)⟩
id              └──────┘ └─┘          └──────────┘    
src             └──────┘ └─┘             └──────────┘    
typ             └──────┘ └─┘          └──────────┘    
doc             └──────┘ └─┘             └──────────┘
707  
708  instance : metric_space ℚ_[p] :=
id              └──────────┘ └─┘
src             └──────────┘ └─┘ 
typ             └──────────┘ └─┘
doc             └──────────┘ └─┘ 
709  { dist_self := by simp [dist],
id   
src                   └────┘    
typ                   └────┘    
doc                    └────┘    
txt                    └────┘    
par                    └────┘    
pid                            
st                    └──────────┘
710    dist_comm := λ x y, by unfold dist; rw ←padic_norm_e.neg (x - y); simp,
id                                           └──────────────┘    
src                           └─────────┘  └──┘└──────────────┘     └──┘
typ                         └─────────┘  └──┘└──────────────┘   └──┘
doc                           └─────────┘  └──┘                      └──┘
txt                           └─────────┘  └──┘                      └──┘
par                           └─────────┘  └──┘                      └──┘
pid                                 └───┘    └┘                    
st                           └──────────────────────────────────────────────┘
711    dist_triangle :=
712      begin
st       └─────
713        intros, unfold dist,
src        └────┘  └─────────┘
typ        └────┘  └─────────┘
doc        └────┘  └─────────┘
txt        └────┘  └─────────┘
par        └────┘  └─────────┘
pid                      └───┘
st   ───────────┘└───────────┘└─
714        exact_mod_cast padic_norm_e.triangle_ineq _ _ _,
id                        └────────────────────────┘
src        └─────────────┘└────────────────────────┘└────┘
typ        └─────────────┘└────────────────────────┘└────┘
doc        └─────────────┘                          └────┘
txt        └─────────────┘                          └────┘
par        └─────────────┘                          └────┘
pid                                                └────┘
st   ────────────────────────────────────────────────────┘└─
715      end,
st   ──────┘
716    eq_of_dist_eq_zero :=
717      begin
st       └─────
718        unfold dist, intros _ _ h,
src        └─────────┘  └──────────┘
typ        └─────────┘  └──────────┘
doc        └─────────┘  └──────────┘
txt        └─────────┘  └──────────┘
par        └─────────┘  └──────────┘
pid              └───┘        └────┘
st   ────────────────┘└────────────┘└─
719        apply eq_of_sub_eq_zero,
id               └───────────────┘
src        └────┘└───────────────┘
typ        └────┘└───────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────┘└─
720        apply (padic_norm_e.zero_iff _).1,
id                └───────────────────┘
src        └────┘ └───────────────────┘└───┘
typ        └────┘ └───────────────────┘└───┘
doc        └────┘                      └───┘
txt        └────┘                      └───┘
par        └────┘                      └───┘
pid                                   └─┘└┘
st   ──────────────────────────────────────┘└─
721        exact_mod_cast h
id                        
src        └─────────────┘ 
typ        └─────────────┘
doc        └─────────────┘ 
txt        └─────────────┘ 
par        └─────────────┘ 
pid                       
st   ───────────────────────
722      end }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
723  
724  instance : has_norm ℚ_[p] := ⟨λ x, padic_norm_e x⟩
id              └──────┘ └─┘         └──────────┘ 
src             └──────┘ └─┘           └──────────┘
typ             └──────┘ └─┘         └──────────┘ 
doc             └──────┘ └─┘           └──────────┘
725  
726  instance : normed_field ℚ_[p] :=
id              └──────────┘ └─┘
src             └──────────┘ └─┘ 
typ             └──────────┘ └─┘
doc             └──────────┘ └─┘ 
727  { dist_eq := λ _ _, rfl,
id                     └─┘
src                      └─┘
typ                    └─┘
728    norm_mul' := by simp [has_norm.norm, padic_norm_e.mul'] }
id                                          └───────────────┘
src                                        └───────────────┘
typ                                        └───────────────┘
doc                    
txt                    
par                    
st                    └┘     └───────────┘  └───────────────┘
729  
730  instance : is_absolute_value (λ a : ℚ_[p], ∥a∥) :=
id              └───────────────┘        └─┘  
src             └───────────────┘        └─┘    
typ             └───────────────┘        └─┘  
doc             └───────────────┘        └─┘ 
731  { abv_nonneg := norm_nonneg,
id                   └─────────┘
src                  └─────────┘
typ                  └─────────┘
732    abv_eq_zero := norm_eq_zero,
id                    └──────────┘
src                   └──────────┘
typ                   └──────────┘
733    abv_add := norm_add_le,
id                └─────────┘
src               └─────────┘
typ               └─────────┘
doc               └─────────┘
734    abv_mul := by simp [has_norm.norm, padic_norm_e.mul'] }
id                                        └───────────────┘
src                                       └───────────────┘
typ                                       └───────────────┘
st                        └────┘ └─┘ └┘  └─┘       
735  
736  theorem rat_dense {p : ℕ} {hp : p.prime} (q : ℚ_[p]) {ε : ℝ} (hε : ε > 0) :
id                                  └────┘       └─┘                
src                                  └────┘       └─┘                  
typ                                 └────┘       └─┘                
doc                                   └────┘       └─┘ 
737          ∃ r : ℚ, ∥q - r∥ < ε :=
id                     
src                     
typ                    
doc                
738  let ⟨ε', hε'l, hε'r⟩ := exists_rat_btwn hε,
id                  └──┘                     └┘
typ                 └──┘                     └┘
739      ⟨r, hr⟩ := rat_dense' q (by simpa using hε'l)  in
id                 └────────┘ 
src                 └────────┘
typ                └────────┘ 
740  ⟨r, lt.trans (by simpa [has_norm.norm] using hr) hε'r⟩
id       └──────┘                                 
src      └──────┘
typ      └──────┘                                 
741  
742  end normed_space
743  end padic
744  
745  namespace padic_norm_e
746  section normed_space
747  variables {p : ℕ} [hp : p.prime]
id                           └────┘
src                          └────┘
typ                          └────┘
doc                           └────┘
748  include hp
749  
750  @[simp] protected lemma mul (q r : ℚ_[p]) : ∥q * r∥ = ∥q∥ * ∥r∥ :=
id                                      └─┘          
src                                     └─┘               
typ                                     └─┘          
doc    └──┘                             └─┘ 
751  by simp [has_norm.norm, padic_norm_e.mul']
st     
752  
753  protected lemma is_norm (q : ℚ_[p]) : ↑(padic_norm_e q) = ∥q∥ := rfl
id                                                            
typ                                                           
754  
755  theorem nonarchimedean (q r : ℚ_[p]) : ∥q + r∥ ≤ max (∥q∥) (∥r∥) :=
id                                                       
typ                                                      
756  begin
757    unfold has_norm.norm,
758    exact_mod_cast nonarchimedean' _ _
759  end
st   └─┘
760  
761  theorem add_eq_max_of_ne {q r : ℚ_[p]} (h : ∥q∥ ≠ ∥r∥) : ∥q+r∥ = max (∥q∥) (∥r∥) :=
id                                                                      
typ                                                                     
762  begin
763    unfold has_norm.norm,
764    apply_mod_cast add_eq_max_of_ne',
765    intro h',
766    apply h,
767    unfold has_norm.norm,
768    exact_mod_cast h'
769  end
st   └─┘
770  
771  @[simp] lemma eq_padic_norm (q : ℚ) : ∥(↑q : ℚ_[p])∥ = padic_norm p q :=
id                                                                   
src                                   
typ                                                                  
doc    └──┘                           
772  begin
773    unfold has_norm.norm,
774    rw [← padic_norm_e.eq_padic_norm', ← padic.cast_eq_of_rat]
st                                                              
775  end
st   └─┘
776  
777  instance : nondiscrete_normed_field ℚ_[p] :=
id              └┘  └┘  └┘  └┘  └┘  └┘      
src             └┘  └┘  └┘  └┘  └┘  └┘
typ             └┘  └┘  └┘  └┘  └┘  └┘      
doc             └┘  └┘  └┘  └┘  └┘  └┘
778  { non_trivial := ⟨padic.of_rat p (p⁻¹), begin
id                                    
typ                                   
779      have h0 : p ≠ 0 := ne_of_gt (hp.pos),
id                 
typ                
780      have h1 : 1 < p := hp.one_lt,
id                     
typ                    
781      rw [← padic.cast_eq_of_rat, eq_padic_norm],
782      simp only [padic_norm, inv_eq_zero],
id                  └────────┘
src                 └────────┘
typ                 └────────┘
doc                 └────────┘
783      simp only [if_neg] {discharger := `[exact_mod_cast h0]},
784      norm_cast,
785      simp only [padic_val_rat.inv] {discharger := `[exact_mod_cast h0]},
786      rw [neg_neg, padic_val_rat.padic_val_rat_self h1],
787      erw _root_.pow_one,
788      exact_mod_cast h1,
789    end⟩ }
st     └─┘
790  
791  
792  protected theorem image {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, ∥q∥ = ↑((↑p : ℚ) ^ (-n)) :=
id                                                                         
src                                                                      
typ                                                                        
doc                                                                       
793  quotient.induction_on q $ λ f hf,
id                         
typ                        
794    have ¬ f ≈ 0, from (padic_seq.ne_zero_iff_nequiv_zero f).1 hf,
id          
src         
typ         
795    let ⟨n, hn⟩ := padic_seq.norm_image f this in
id          
typ         
796    ⟨n, congr_arg rat.cast hn⟩
797  
798  protected lemma is_rat (q : ℚ_[p]) : ∃ q' : ℚ, ∥q∥ = ↑q' :=
id                                                      └┘
src                                              
typ                                                     └┘
doc                                              
799  if h : q = 0 then ⟨0, by simp [h]⟩
800  else let ⟨n, hn⟩ := padic_norm_e.image h in ⟨_, hn⟩
801  
802  def rat_norm (q : ℚ_[p]) : ℚ := classical.some (padic_norm_e.is_rat q)
id                                                                     
src                             
typ                                                                    
doc                             
803  
804  lemma eq_rat_norm (q : ℚ_[p]) : ∥q∥ = rat_norm q := classical.some_spec (padic_norm_e.is_rat q)
id                                                                                             
typ                                                                                            
805  
806  theorem norm_rat_le_one : ∀ {q : ℚ} (hq : ¬ p ∣ q.denom), ∥(q : ℚ_[p])∥ ≤ 1
id                                                 └┘ └─┘           
src                                                  └┘ └─┘
typ                                                └┘ └─┘           
doc                                   
807  | ⟨n, d, hn, hd⟩ := λ hq : ¬ p ∣ d,
id              └┘              
typ             └┘              
808    if hnz : n = 0 then
809      have (⟨n, d, hn, hd⟩ : ℚ) = 0,
id                              
src                             
typ                             
doc                             
810      from rat.zero_iff_num_zero.mpr hnz,
811      by norm_num [this]
812    else
813      begin
814        have hnz' : {rat . num := n, denom := d, pos := hn, cop := hd} ≠ 0, from mt rat.zero_iff_num_zero.1 hnz,
id                                                                   └┘
typ                                                                  └┘
815        rw [padic_norm_e.eq_padic_norm],
816        norm_cast,
817        rw [padic_norm.eq_fpow_of_nonzero p hnz', padic_val_rat_def p hnz'],
id                                                                    
typ                                                                   
818        have h : (multiplicity p d).get _ = 0, by simp [multiplicity_eq_zero_of_not_dvd, hq],
id                                 
typ                                
819        rw_mod_cast [h, sub_zero],
820        apply fpow_le_one_of_nonpos,
821        { exact_mod_cast le_of_lt hp.one_lt, },
st                                              └┘
822        { apply neg_nonpos_of_nonneg, norm_cast, simp, }
st                                                        └┘
823      end
824  
825  lemma eq_of_norm_add_lt_right {p : ℕ} {hp : p.prime} {z1 z2 : ℚ_[p]}
id                                              └──┘                
src                                              └──┘
typ                                             └──┘                
doc                                               └──┘
826    (h : ∥z1 + z2∥ < ∥z2∥) : ∥z1∥ = ∥z2∥ :=
id           └┘         └┘      └┘      
typ          └┘         └┘      └┘      
827  by_contradiction $ λ hne,
828    not_lt_of_ge (by rw padic_norm_e.add_eq_max_of_ne hne; apply le_max_right) h
829  
830  lemma eq_of_norm_add_lt_left {p : ℕ} {hp : p.prime} {z1 z2 : ℚ_[p]}
id                                             └───┘               
src                                             └───┘
typ                                            └───┘               
doc                                              └───┘
831    (h : ∥z1 + z2∥ < ∥z1∥) : ∥z1∥ = ∥z2∥ :=
id           └┘         └┘      └┘      
typ          └┘         └┘      └┘      
832  by_contradiction $ λ hne,
833    not_lt_of_ge (by rw padic_norm_e.add_eq_max_of_ne hne; apply le_max_left) h
834  
835  end normed_space
836  end padic_norm_e
837  
838  namespace padic
839  variables {p : ℕ} [nat.prime p]
id                     └──┘  └─┘
src                    └──┘  └─┘
typ                    └──┘  └─┘
doc                     └──┘  └─┘
840  
841  set_option eqn_compiler.zeta true
doc             └───────────────┘
842  instance complete : cau_seq.is_complete ℚ_[p] norm :=
id                                              
typ                                             
843  begin
844    split, intro f,
845    have cau_seq_norm_e : is_cau_seq padic_norm_e f,
846    { intros ε hε,
847      let h := is_cau f ε (by exact_mod_cast hε),
id                         
typ                        
848      unfold norm at h,
849      apply_mod_cast h },
st                        └┘
850    cases padic.complete' ⟨f, cau_seq_norm_e⟩ with q hq,
851    existsi q,
id             
typ            
852    intros ε hε,
853    cases exists_rat_btwn hε with ε' hε',
854    norm_cast at hε',
855    cases hq ε' hε'.1 with N hN, existsi N,
id              └┘                          
typ             └┘                          
856    intros i hi, let h := hN i hi,
id                               └┘
typ                              └┘
857    unfold norm,
858    rw_mod_cast [cau_seq.sub_apply, padic_norm_e.sub_rev],
859    refine lt.trans _ hε'.2,
860    exact_mod_cast hN i hi
id                        └┘
typ                       └┘
861  end
st   └─┘
862  
863  lemma padic_norm_e_lim_le {f : cau_seq ℚ_[p] norm} {a : ℝ} (ha : a > 0)
id                                                                  
src                                                          
typ                                                                 
864        (hf : ∀ i, ∥f i∥ ≤ a) : ∥f.lim∥ ≤ a :=
id                                        
typ                                       
865  let ⟨N, hN⟩ := setoid.symm (cau_seq.equiv_lim f) _ ha in
id        
typ       
866  calc ∥f.lim∥ = ∥f.lim - f N + f N∥ : by simp
867                  ... ≤ max (∥f.lim - f N∥) (∥f N∥) : padic_norm_e.nonarchimedean _ _
868                  ... ≤ a : max_le (le_of_lt (hN _ (le_refl _))) (hf _)
id                         
typ                        
869  
870  end padic